Wolfram Research

Function Repository Resource:

ModusPonensToEquational

Source Notebook

Convert an axiom system from modus ponens to equational form

Contributed by: Matthew Szudzik & Stephen Wolfram

ResourceFunction["ModusPonensToEquational"][axioms, implies]

converts the specified list of modus ponens axioms to equational form, taking implies to be the representation of implication.

Details and Options

ModusPonensToEquational removes implicit use of modus ponens {x, xy}y as a rule of inference. It generates pure equational axioms which rely only on substitution.

Examples

Basic Examples

Convert the Lukasiewicz modus ponens axiom system to equational form:

In[1]:=
ResourceFunction[
 "ModusPonensToEquational"][{imp[
   imp[imp[a, imp[b, a]], imp[imp[imp[not[c], imp[d, not[e]]], imp[imp[c, imp[d, f]], imp[imp[e, d], imp[e, f]]]], g]], imp[h, g]]}, imp]
Out[1]=

Convert to Hilbert-Ackermann axiom system for propositional logic, giving a function for implies:

In[2]:=
ResourceFunction["ModusPonensToEquational"][{or[not[or[a, a]], a],
  or[not[a], or[a, b]],
  or[not[or[a, b]], or[b, a]],
  or[not[or[not[a], b]], or[not[or[c, a]], or[c, b]]]}, or[not[#1], #2] &]
Out[2]=

Requirements

Wolfram Language 11.3 (March 2018) or above

Resource History

License Information