Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

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, x→y}→y as a rule of inference. It generates pure equational axioms that rely only on substitution.

Examples

Basic Examples (2) 

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 the 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

Version History

  • 1.0.0 – 29 November 2018

Source Metadata

  • Citation:
    • Stephen Wolfram (2002), A New Kind of Science

License Information