OpenMath Content Dictionary: logic3

Canonical URL:

http://www.openmath.org/cd/logic3.ocd

CD File:

logic3.ocd

CD as XML Encoded OpenMath:

logic3.omcd

Defines:

Generalisation, Hypothesis, ModusPonens, axiom_instance, complete_pred_deduction, complete_pred_theorem, complete_prop_deduction, complete_prop_theorem, is_deduction, is_theorem, pred_deduction, pred_theorem, proof, prop_deduction, prop_theorem

Date:

2001-07-31

Version:

0 (Revision 2)

Review Date:

2017-12-31

Status:

experimental

---

     This document is distributed in the hope that it will be useful, 
     but WITHOUT ANY WARRANTY; without even the implied warranty of 
     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

     The copyright holder grants you permission to redistribute this 
     document freely as a verbatim copy. Furthermore, the copyright
     holder permits you to develop any derived work from this document
     provided that the following conditions are met.
       a) The derived work acknowledges the fact that it is derived from
          this document, and maintains a prominent reference in the 
          work to the original source.
       b) The fact that the derived work is not the original OpenMath 
          document is stated prominently in the derived work.  Moreover if
          both this document and the derived work are Content Dictionaries
          then the derived work must include a different CDName element,
          chosen so that it cannot be confused with any works adopted by
          the OpenMath Society.  In particular, if there is a Content 
          Dictionary Group whose name is, for example, `math' containing
          Content Dictionaries named `math1', `math2' etc., then you should 
          not name a derived Content Dictionary `mathN' where N is an integer.
          However you are free to name it `private_mathN' or some such.  This
          is because the names `mathN' may be used by the OpenMath Society
          for future extensions.
       c) The derived work is distributed under terms that allow the
          compilation of derived works, but keep paragraphs a) and b)
          intact.  The simplest way to do this is to distribute the derived
          work under the OpenMath license, but this is not a requirement.
     If you have questions about this license please contact the OpenMath
     society at http://www.openmath.org.

  Author: James Davenport and Bill Naylor

This CD holds the symbols for constructing formal proofs in the (classical) propositional and predicate calculus (first-order).

---

prop_theorem

Description:

This symbol is used to claim that a statement is a theorem of the classical propositional calculus, i.e. that it follows by applications of Modus Ponens from instantiations of the axioms (which may be the common three involving 'implies', but need not be).

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="prop_theorem"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="A"/>
      <OMV name="A"/>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">prop_theorem</csymbol>
  <apply><csymbol cd="logic1">implies</csymbol><ci>A</ci><ci>A</ci></apply>
 </apply>
</math>

Prefix

prop_theorem (implies ( A, A) )

Popcorn

logic3.prop_theorem($A ==> $A)

Rendered Presentation MathML

$$\mathrm{prop\_theorem}\left(A\Rightarrow A\right)$$

Signatures:

sts

---

[Next: pred_theorem] [Last: is_deduction] [Top]

---

pred_theorem

Description:

This symbol is used to claim that a statement is a theorem of the classical first-order predicate calculus, i.e. that it follows by applications of Modus Ponens, and generalisation from instantiations of the Axioms (which may be the common three involving 'implies', together with forall-instantiation and moving forall inside implication, but need not be).

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="pred_theorem"/>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMV name="P"/>
          <OMV name="x"/>
        </OMA>
        <OMA>
          <OMV name="P"/>
          <OMV name="x"/>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">pred_theorem</csymbol>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>x</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><ci>P</ci><ci>x</ci></apply>
    <apply><ci>P</ci><ci>x</ci></apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

pred_theorem (forall [ x ] . (implies ( P ( x) , P ( x) ) ) )

Popcorn

logic3.pred_theorem(quant1.forall[$x -> $P($x) ==> $P($x)])

Rendered Presentation MathML

$$\mathrm{pred\_theorem}\left(\forall \hspace{0.17em}x.P\left(x\right)\Rightarrow P\left(x\right)\right)$$

Signatures:

sts

---

[Next: is_theorem] [Previous: prop_theorem] [Top]

---

is_theorem

Description:

This symbol expresses whether or not there is a theorem of the form quoted. Hence for items of type complete_prop_theorem, it is always true

Signatures:

sts

---

[Next: axiom_instance] [Previous: pred_theorem] [Top]

---

axiom_instance

Description:

This symbol represents a line in a formal proof which is an instance of an axiom. The first child is the line in the proof: the second is the axiom used.

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="logic3" name="axiom_instance"/>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="a"/>
      <OMV name="a"/>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="a"/>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMV name="a"/>
        <OMV name="a"/>
      </OMA>
    </OMA>
  </OMA>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMV name="a"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="b"/>
      <OMV name="a"/>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">axiom_instance</csymbol>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
   <apply><csymbol cd="logic1">implies</csymbol>
    <ci>a</ci>
    <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
   </apply>
  </apply>
  <apply><csymbol cd="logic1">implies</csymbol>
   <ci>a</ci>
   <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>a</ci></apply>
  </apply>
 </apply>
</math>

Prefix

axiom_instance (implies (implies ( a, a) , implies ( a, implies ( a, a) ) ) , implies ( a, implies ( b, a) ) )

Popcorn

logic3.axiom_instance($a ==> $a ==> $a ==> $a ==> $a, $a ==> $b ==> $a)

Rendered Presentation MathML

$$\mathrm{axiom\_instance}(a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a,a\Rightarrow b\Rightarrow a)$$

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="logic3" name="axiom_instance"/>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="a"/>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMV name="a"/>
          <OMV name="a"/>
        </OMA>
        <OMV name="a"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMV name="a"/>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMV name="a"/>
          <OMV name="a"/>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMV name="a"/>
        <OMV name="a"/>
      </OMA>
    </OMA>
  </OMA>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="a"/>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMV name="b"/>
        <OMV name="c"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMV name="a"/>
        <OMV name="b"/>
      </OMA>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMV name="a"/>
        <OMV name="c"/>
      </OMA>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">axiom_instance</csymbol>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="logic1">implies</csymbol>
    <ci>a</ci>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
     <ci>a</ci>
    </apply>
   </apply>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">implies</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
    </apply>
    <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
   </apply>
  </apply>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="logic1">implies</csymbol>
    <ci>a</ci>
    <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>c</ci></apply>
   </apply>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>b</ci></apply>
    <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>c</ci></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

axiom_instance (implies (implies ( a, implies (implies ( a, a) , a) ) , implies (implies ( a, implies ( a, a) ) , implies ( a, a) ) ) , implies (implies ( a, implies ( b, c) ) , implies (implies ( a, b) , implies ( a, c) ) ) )

Popcorn

logic3.axiom_instance($a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a, $a ==> $b ==> $c ==> $a ==> $b ==> $a ==> $c)

Rendered Presentation MathML

$$\mathrm{axiom\_instance}(a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a,a\Rightarrow b\Rightarrow c\Rightarrow a\Rightarrow b\Rightarrow a\Rightarrow c)$$

Note how the issue of substitution is dealt with in the specification
of axiom 4 of the predicate calculus. Essentially, it has to be
assumed that beta-reduction takes place when the axiom is instantiated.

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="logic3" name="axiom_instance"/>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMS name="eq" cd="relation1"/>
          <OMV name="x"/>
          <OMS name="zero" cd="alg1"/>
        </OMA>
        <OMA>
          <OMS name="eq" cd="relation1"/>
          <OMA>
            <OMS name="times" cd="arith1"/>
            <OMV name="x"/>
            <OMV name="x"/>
          </OMA>
          <OMS name="zero" cd="alg1"/>
        </OMA>
      </OMA>
    </OMBIND>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS name="eq" cd="relation1"/>
        <OMA>
          <OMS name="plus" cd="arith1"/>
          <OMV name="x"/>
          <OMS name="one" cd="alg1"/>
        </OMA>
        <OMS name="zero" cd="alg1"/>
      </OMA>
      <OMA>
        <OMS name="eq" cd="relation1"/>
        <OMA>
          <OMS name="times" cd="arith1"/>
          <OMA>
            <OMS name="plus" cd="arith1"/>
            <OMV name="x"/>
            <OMS name="one" cd="alg1"/>
          </OMA>
          <OMA>
            <OMS name="plus" cd="arith1"/>
            <OMV name="x"/>
            <OMS name="one" cd="alg1"/>
          </OMA>
        </OMA>
        <OMS name="zero" cd="alg1"/>
      </OMA>
    </OMA>
  </OMA>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMV name="S"/>
    </OMBIND>
    <OMA>
      <OMBIND>
        <OMS cd="fns1" name="lambda"/>
        <OMBVAR>
          <OMV name="x"/>
        </OMBVAR>
        <OMV name="S"/>
      </OMBIND>
      <OMV name="T"/>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">axiom_instance</csymbol>
  <apply><csymbol cd="logic1">implies</csymbol>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>x</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="relation1">eq</csymbol><ci>x</ci><csymbol cd="alg1">zero</csymbol></apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="arith1">times</csymbol><ci>x</ci><ci>x</ci></apply>
      <csymbol cd="alg1">zero</csymbol>
     </apply>
    </apply>
   </bind>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="arith1">plus</csymbol><ci>x</ci><csymbol cd="alg1">one</csymbol></apply>
     <csymbol cd="alg1">zero</csymbol>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="arith1">times</csymbol>
      <apply><csymbol cd="arith1">plus</csymbol><ci>x</ci><csymbol cd="alg1">one</csymbol></apply>
      <apply><csymbol cd="arith1">plus</csymbol><ci>x</ci><csymbol cd="alg1">one</csymbol></apply>
     </apply>
     <csymbol cd="alg1">zero</csymbol>
    </apply>
   </apply>
  </apply>
  <apply><csymbol cd="logic1">implies</csymbol>
   <bind><csymbol cd="quant1">forall</csymbol><bvar><ci>x</ci></bvar><ci>S</ci></bind>
   <apply>
    <bind><csymbol cd="fns1">lambda</csymbol><bvar><ci>x</ci></bvar><ci>S</ci></bind>
    <ci>T</ci>
   </apply>
  </apply>
 </apply>
</math>

Prefix

axiom_instance (implies (forall [ x ] . (implies (eq ( x, zero) , eq (times ( x, x) , zero) ) ) , implies (eq (plus ( x, one) , zero) , eq (times (plus ( x, one) , plus ( x, one) ) , zero) ) ) , implies (forall [ x ] . ( S) , lambda [ x ] . ( S) ( T) ) )

Popcorn

logic3.axiom_instance(quant1.forall[$x -> $x = alg1.zero ==> $x * $x = alg1.zero] ==> $x + alg1.one = alg1.zero ==> ($x + alg1.one) * ($x + alg1.one) = alg1.zero, quant1.forall[$x -> $S] ==> fns1.lambda[$x -> $S]($T))

Rendered Presentation MathML

$$\mathrm{axiom\_instance}(\forall \hspace{0.17em}x.x=0\Rightarrow xx=0\Rightarrow x+1=0\Rightarrow (x+1)(x+1)=0,\forall \hspace{0.17em}x.S\Rightarrow \lambda \hspace{0.17em}x.S)$$

Signatures:

sts

---

[Next: ModusPonens] [Previous: is_theorem] [Top]

---

ModusPonens

Description:

This symbol represents the generation of a line of a proof by application of Modus Ponens. The first argument is the new well-formed formula (B), the second is the line number in the proof for A and the third is the line number in the proof for A implies B.

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="ModusPonens"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="a"/>
      <OMV name="a"/>
    </OMA>
    <OMI> 4 </OMI>
    <OMI> 2 </OMI>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">ModusPonens</csymbol>
  <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
  <cn type="integer">4</cn>
  <cn type="integer">2</cn>
 </apply>
</math>

Prefix

ModusPonens (implies ( a, a) , 4 , 2 )

Popcorn

logic3.ModusPonens($a ==> $a, 4, 2)

Rendered Presentation MathML

$$\mathrm{ModusPonens}(a\Rightarrow a,4,2)$$

Signatures:

sts

---

[Next: Generalisation] [Previous: axiom_instance] [Top]

---

Generalisation

Description:

This symbol represents the generation of a line of a proof by application of Generalisation. The first argument is the new well-formed formula (forall x.B) and the second is the line number in the proof for B.

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="Generalisation"/>
    <OMBIND>
      <OMS name="forall" cd="quant1"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMV name="P"/>
          <OMV name="x"/>
        </OMA>
        <OMA>
          <OMV name="P"/>
          <OMV name="x"/>
        </OMA>
      </OMA>
    </OMBIND>
    <OMI> 5 </OMI>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">Generalisation</csymbol>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>x</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><ci>P</ci><ci>x</ci></apply>
    <apply><ci>P</ci><ci>x</ci></apply>
   </apply>
  </bind>
  <cn type="integer">5</cn>
 </apply>
</math>

Prefix

Generalisation (forall [ x ] . (implies ( P ( x) , P ( x) ) ) , 5 )

Popcorn

logic3.Generalisation(quant1.forall[$x -> $P($x) ==> $P($x)], 5)

Rendered Presentation MathML

$$\mathrm{Generalisation}(\forall \hspace{0.17em}x.P\left(x\right)\Rightarrow P\left(x\right),5)$$

Signatures:

sts

---

[Next: Hypothesis] [Previous: ModusPonens] [Top]

---

Hypothesis

Description:

This symbol represents that a wellformed formula is a hypothesis of a deduction of the propositional or predicate calculus.

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="Hypothesis"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="a"/>
      <OMV name="a"/>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">Hypothesis</csymbol>
  <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
 </apply>
</math>

Prefix

Hypothesis (implies ( a, a) )

Popcorn

logic3.Hypothesis($a ==> $a)

Rendered Presentation MathML

$$\mathrm{Hypothesis}\left(a\Rightarrow a\right)$$

Signatures:

sts

---

[Next: proof] [Previous: Generalisation] [Top]

---

proof

Description:

This symbol represents a sequence of justified well-formed formulae (i.e. objects of type ProofLine). The single argument is a List of ProofLine objects.

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="proof"/>
    <OMA>
      <OMS cd="list1" name="list"/>
      <OMA>
        <OMS cd="logic3" name="axiom_instance"/>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="a"/>
              </OMA>
              <OMV name="a"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="a"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="b"/>
              <OMV name="c"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMV name="b"/>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMV name="c"/>
            </OMA>
          </OMA>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="logic3" name="axiom_instance"/>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMV name="a"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMV name="a"/>
            </OMA>
            <OMV name="a"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMV name="a"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="b"/>
            <OMV name="a"/>
          </OMA>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="logic3" name="ModusPonens"/>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMV name="a"/>
          </OMA>
        </OMA>
        <OMI> 2 </OMI>
        <OMI> 1 </OMI>
      </OMA>
      <OMA>
        <OMS cd="logic3" name="axiom_instance"/>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMV name="a"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMV name="a"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMV name="a"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="b"/>
            <OMV name="a"/>
          </OMA>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="logic3" name="ModusPonens"/>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMV name="a"/>
          <OMV name="a"/>
        </OMA>
        <OMI> 4 </OMI>
        <OMI> 3 </OMI>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">proof</csymbol>
  <apply><csymbol cd="list1">list</csymbol>
   <apply><csymbol cd="logic3">axiom_instance</csymbol>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
       <ci>a</ci>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
      </apply>
      <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>c</ci></apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>b</ci></apply>
      <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>c</ci></apply>
     </apply>
    </apply>
   </apply>
   <apply><csymbol cd="logic3">axiom_instance</csymbol>
    <apply><csymbol cd="logic1">implies</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
      <ci>a</ci>
     </apply>
    </apply>
    <apply><csymbol cd="logic1">implies</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>a</ci></apply>
    </apply>
   </apply>
   <apply><csymbol cd="logic3">ModusPonens</csymbol>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
    </apply>
    <cn type="integer">2</cn>
    <cn type="integer">1</cn>
   </apply>
   <apply><csymbol cd="logic3">axiom_instance</csymbol>
    <apply><csymbol cd="logic1">implies</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
    </apply>
    <apply><csymbol cd="logic1">implies</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>a</ci></apply>
    </apply>
   </apply>
   <apply><csymbol cd="logic3">ModusPonens</csymbol>
    <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
    <cn type="integer">4</cn>
    <cn type="integer">3</cn>
   </apply>
  </apply>
 </apply>
</math>

Prefix

proof (list (axiom_instance (implies (implies ( a, implies (implies ( a, a) , a) ) , implies (implies ( a, implies ( a, a) ) , implies ( a, a) ) ) , implies (implies ( a, implies ( b, c) ) , implies (implies ( a, b) , implies ( a, c) ) ) ) , axiom_instance (implies ( a, implies (implies ( a, a) , a) ) , implies ( a, implies ( b, a) ) ) , ModusPonens (implies (implies ( a, implies ( a, a) ) , implies ( a, a) ) , 2 , 1 ) , axiom_instance (implies ( a, implies ( a, a) ) , implies ( a, implies ( b, a) ) ) , ModusPonens (implies ( a, a) , 4 , 3 ) ) )

Popcorn

logic3.proof([logic3.axiom_instance($a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a, $a ==> $b ==> $c ==> $a ==> $b ==> $a ==> $c) , logic3.axiom_instance($a ==> $a ==> $a ==> $a, $a ==> $b ==> $a) , logic3.ModusPonens($a ==> $a ==> $a ==> $a ==> $a, 2, 1) , logic3.axiom_instance($a ==> $a ==> $a, $a ==> $b ==> $a) , logic3.ModusPonens($a ==> $a, 4, 3)])

Rendered Presentation MathML

$$\mathrm{proof}\left(\begin{array}{c}\mathrm{axiom\_instance}(a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a,a\Rightarrow b\Rightarrow c\Rightarrow a\Rightarrow b\Rightarrow a\Rightarrow c)\hfill \\ \mathrm{axiom\_instance}(a\Rightarrow a\Rightarrow a\Rightarrow a,a\Rightarrow b\Rightarrow a)\hfill \\ \mathrm{ModusPonens}(a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a,2,1)\hfill \\ \mathrm{axiom\_instance}(a\Rightarrow a\Rightarrow a,a\Rightarrow b\Rightarrow a)\hfill \\ \mathrm{ModusPonens}(a\Rightarrow a,4,3)\hfill \end{array}\right)$$

Signatures:

sts

---

[Next: complete_prop_theorem] [Previous: Hypothesis] [Top]

---

complete_prop_theorem

Description:

This symbol is used to state, with proof (the second child), that a statement (the first child) is a theorem of the classical propositional calculus, i.e. that it follows by applications of Modus Ponens from instantiations of the axioms (which may be the common three involving 'implies', but need not be).

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="complete_prop_theorem"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="A"/>
      <OMV name="A"/>
    </OMA>
    <OMA>
      <OMS cd="logic3" name="proof"/>
      <OMA>
        <OMS cd="list1" name="list"/>
        <OMA>
          <OMS cd="logic3" name="axiom_instance"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMA>
                  <OMS cd="logic1" name="implies"/>
                  <OMV name="a"/>
                  <OMV name="a"/>
                </OMA>
                <OMV name="a"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMA>
                  <OMS cd="logic1" name="implies"/>
                  <OMV name="a"/>
                  <OMV name="a"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="a"/>
              </OMA>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="b"/>
                <OMV name="c"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="b"/>
              </OMA>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="c"/>
              </OMA>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic3" name="axiom_instance"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="a"/>
              </OMA>
              <OMV name="a"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="b"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic3" name="ModusPonens"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="a"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
          <OMI> 2 </OMI>
          <OMI> 1 </OMI>
        </OMA>
        <OMA>
          <OMS cd="logic3" name="axiom_instance"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="b"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic3" name="ModusPonens"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMV name="a"/>
          </OMA>
          <OMI> 4 </OMI>
          <OMI> 3 </OMI>
        </OMA>
      </OMA>
    </OMA> 
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">complete_prop_theorem</csymbol>
  <apply><csymbol cd="logic1">implies</csymbol><ci>A</ci><ci>A</ci></apply>
  <apply><csymbol cd="logic3">proof</csymbol>
   <apply><csymbol cd="list1">list</csymbol>
    <apply><csymbol cd="logic3">axiom_instance</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="logic1">implies</csymbol>
        <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
        <ci>a</ci>
       </apply>
      </apply>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><csymbol cd="logic1">implies</csymbol>
        <ci>a</ci>
        <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
       </apply>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>c</ci></apply>
      </apply>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>b</ci></apply>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>c</ci></apply>
      </apply>
     </apply>
    </apply>
    <apply><csymbol cd="logic3">axiom_instance</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
       <ci>a</ci>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>a</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="logic3">ModusPonens</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
      </apply>
      <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
     </apply>
     <cn type="integer">2</cn>
     <cn type="integer">1</cn>
    </apply>
    <apply><csymbol cd="logic3">axiom_instance</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>a</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="logic3">ModusPonens</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>a</ci></apply>
     <cn type="integer">4</cn>
     <cn type="integer">3</cn>
    </apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

complete_prop_theorem (implies ( A, A) , proof (list (axiom_instance (implies (implies ( a, implies (implies ( a, a) , a) ) , implies (implies ( a, implies ( a, a) ) , implies ( a, a) ) ) , implies (implies ( a, implies ( b, c) ) , implies (implies ( a, b) , implies ( a, c) ) ) ) , axiom_instance (implies ( a, implies (implies ( a, a) , a) ) , implies ( a, implies ( b, a) ) ) , ModusPonens (implies (implies ( a, implies ( a, a) ) , implies ( a, a) ) , 2 , 1 ) , axiom_instance (implies ( a, implies ( a, a) ) , implies ( a, implies ( b, a) ) ) , ModusPonens (implies ( a, a) , 4 , 3 ) ) ) )

Popcorn

logic3.complete_prop_theorem($A ==> $A, logic3.proof([logic3.axiom_instance($a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a ==> $a, $a ==> $b ==> $c ==> $a ==> $b ==> $a ==> $c) , logic3.axiom_instance($a ==> $a ==> $a ==> $a, $a ==> $b ==> $a) , logic3.ModusPonens($a ==> $a ==> $a ==> $a ==> $a, 2, 1) , logic3.axiom_instance($a ==> $a ==> $a, $a ==> $b ==> $a) , logic3.ModusPonens($a ==> $a, 4, 3)]))

Rendered Presentation MathML

$$\mathrm{complete\_prop\_theorem}(A\Rightarrow A,\mathrm{proof}\left(\begin{array}{c}\mathrm{axiom\_instance}(a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a,a\Rightarrow b\Rightarrow c\Rightarrow a\Rightarrow b\Rightarrow a\Rightarrow c)\hfill \\ \mathrm{axiom\_instance}(a\Rightarrow a\Rightarrow a\Rightarrow a,a\Rightarrow b\Rightarrow a)\hfill \\ \mathrm{ModusPonens}(a\Rightarrow a\Rightarrow a\Rightarrow a\Rightarrow a,2,1)\hfill \\ \mathrm{axiom\_instance}(a\Rightarrow a\Rightarrow a,a\Rightarrow b\Rightarrow a)\hfill \\ \mathrm{ModusPonens}(a\Rightarrow a,4,3)\hfill \end{array}\right))$$

Signatures:

sts

---

[Next: complete_pred_theorem] [Previous: proof] [Top]

---

complete_pred_theorem

Description:

This symbol is used to state, with justification, that a statement is a theorem of the classical first-order predicate calculus, i.e. that it follows by applications of Modus Ponens, and generalisation from instantiations of the Axioms (which may be the common three involving 'implies', together with forall-instantiation and moving forall inside implication, but need not be), and the hypotheses (elements of the set which is the second child).

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="complete_pred_theorem"/>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMV name="P"/>
          <OMV name="x"/>
        </OMA>
        <OMA>
          <OMV name="P"/>
          <OMV name="x"/>
        </OMA>
      </OMA>
    </OMBIND>
    <OMA>
      <OMS cd="logic3" name="proof"/>
      <OMA>
        <OMS cd="list1" name="list"/>
        <OMA>
          <OMS cd="logic3" name="axiom_instance"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMV name="P"/>
                <OMV name="x"/>
              </OMA>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMA>
                  <OMS cd="logic1" name="implies"/>
                  <OMA>
                    <OMV name="P"/>
                    <OMV name="x"/>
                  </OMA>
                  <OMA>
                    <OMV name="P"/>
                    <OMV name="x"/>
                  </OMA>
                </OMA>
                <OMA>
                  <OMV name="P"/>
                  <OMV name="x"/>
                </OMA>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMA>
                  <OMV name="P"/>
                  <OMV name="x"/>
                </OMA>
                <OMA>
                  <OMS cd="logic1" name="implies"/>
                  <OMA>
                    <OMV name="P"/>
                    <OMV name="x"/>
                  </OMA>
                  <OMA>
                    <OMV name="P"/>
                    <OMV name="x"/>
                  </OMA>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMA>
                  <OMV name="P"/>
                  <OMV name="x"/>
                </OMA>
                <OMA>
                  <OMV name="P"/>
                  <OMV name="x"/>
                </OMA>
              </OMA>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="a"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="b"/>
                <OMV name="c"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="b"/>
              </OMA>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMV name="a"/>
                <OMV name="c"/>
              </OMA>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic3" name="axiom_instance"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMV name="P"/>
              <OMV name="x"/>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMA>
                  <OMV name="P"/>
                  <OMV name="x"/>
                </OMA>
                <OMA>
                  <OMV name="P"/>
                  <OMV name="x"/>
                </OMA>
              </OMA>
              <OMA>
                <OMV name="P"/>
                <OMV name="x"/>
              </OMA>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="b"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic3" name="ModusPonens"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMV name="P"/>
                <OMV name="x"/>
              </OMA>
              <OMA>
                <OMS cd="logic1" name="implies"/>
                <OMA>
                  <OMV name="P"/>
                  <OMV name="x"/>
                </OMA>
                <OMA>
                  <OMV name="P"/>
                  <OMV name="x"/>
                </OMA>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMV name="P"/>
                <OMV name="x"/>
              </OMA>
              <OMA>
                <OMV name="P"/>
                <OMV name="x"/>
              </OMA>
            </OMA>
          </OMA>
          <OMI> 2 </OMI>
          <OMI> 1 </OMI>
        </OMA>
        <OMA>
          <OMS cd="logic3" name="axiom_instance"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMV name="P"/>
              <OMV name="x"/>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMV name="P"/>
                <OMV name="x"/>
              </OMA>
              <OMA>
                <OMV name="P"/>
                <OMV name="x"/>
              </OMA>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMV name="b"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="logic3" name="ModusPonens"/>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMV name="P"/>
              <OMV name="x"/>
            </OMA>
            <OMA>
              <OMV name="P"/>
              <OMV name="x"/>
            </OMA>
          </OMA>
          <OMI> 4 </OMI>
          <OMI> 3 </OMI>
        </OMA>
      </OMA>
    </OMA> 
    <OMA>
      <OMS cd="logic3" name="Generalisation"/>
      <OMBIND>
        <OMS name="forall" cd="quant1"/>
        <OMBVAR>
          <OMV name="x"/>
        </OMBVAR>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMA>
            <OMV name="P"/>
            <OMV name="x"/>
          </OMA>
          <OMA>
            <OMV name="P"/>
            <OMV name="x"/>
          </OMA>
        </OMA>
      </OMBIND>
      <OMI> 5 </OMI>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">complete_pred_theorem</csymbol>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>x</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><ci>P</ci><ci>x</ci></apply>
    <apply><ci>P</ci><ci>x</ci></apply>
   </apply>
  </bind>
  <apply><csymbol cd="logic3">proof</csymbol>
   <apply><csymbol cd="list1">list</csymbol>
    <apply><csymbol cd="logic3">axiom_instance</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><ci>P</ci><ci>x</ci></apply>
       <apply><csymbol cd="logic1">implies</csymbol>
        <apply><csymbol cd="logic1">implies</csymbol>
         <apply><ci>P</ci><ci>x</ci></apply>
         <apply><ci>P</ci><ci>x</ci></apply>
        </apply>
        <apply><ci>P</ci><ci>x</ci></apply>
       </apply>
      </apply>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><csymbol cd="logic1">implies</csymbol>
        <apply><ci>P</ci><ci>x</ci></apply>
        <apply><csymbol cd="logic1">implies</csymbol>
         <apply><ci>P</ci><ci>x</ci></apply>
         <apply><ci>P</ci><ci>x</ci></apply>
        </apply>
       </apply>
       <apply><csymbol cd="logic1">implies</csymbol>
        <apply><ci>P</ci><ci>x</ci></apply>
        <apply><ci>P</ci><ci>x</ci></apply>
       </apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>c</ci></apply>
      </apply>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>b</ci></apply>
       <apply><csymbol cd="logic1">implies</csymbol><ci>a</ci><ci>c</ci></apply>
      </apply>
     </apply>
    </apply>
    <apply><csymbol cd="logic3">axiom_instance</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><ci>P</ci><ci>x</ci></apply>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><csymbol cd="logic1">implies</csymbol>
        <apply><ci>P</ci><ci>x</ci></apply>
        <apply><ci>P</ci><ci>x</ci></apply>
       </apply>
       <apply><ci>P</ci><ci>x</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>a</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="logic3">ModusPonens</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><ci>P</ci><ci>x</ci></apply>
       <apply><csymbol cd="logic1">implies</csymbol>
        <apply><ci>P</ci><ci>x</ci></apply>
        <apply><ci>P</ci><ci>x</ci></apply>
       </apply>
      </apply>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><ci>P</ci><ci>x</ci></apply>
       <apply><ci>P</ci><ci>x</ci></apply>
      </apply>
     </apply>
     <cn type="integer">2</cn>
     <cn type="integer">1</cn>
    </apply>
    <apply><csymbol cd="logic3">axiom_instance</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><ci>P</ci><ci>x</ci></apply>
      <apply><csymbol cd="logic1">implies</csymbol>
       <apply><ci>P</ci><ci>x</ci></apply>
       <apply><ci>P</ci><ci>x</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="logic1">implies</csymbol><ci>b</ci><ci>a</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="logic3">ModusPonens</csymbol>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><ci>P</ci><ci>x</ci></apply>
      <apply><ci>P</ci><ci>x</ci></apply>
     </apply>
     <cn type="integer">4</cn>
     <cn type="integer">3</cn>
    </apply>
   </apply>
  </apply>
  <apply><csymbol cd="logic3">Generalisation</csymbol>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>x</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><ci>P</ci><ci>x</ci></apply>
     <apply><ci>P</ci><ci>x</ci></apply>
    </apply>
   </bind>
   <cn type="integer">5</cn>
  </apply>
 </apply>
</math>

Prefix

complete_pred_theorem (forall [ x ] . (implies ( P ( x) , P ( x) ) ) , proof (list (axiom_instance (implies (implies ( P ( x) , implies (implies ( P ( x) , P ( x) ) , P ( x) ) ) , implies (implies ( P ( x) , implies ( P ( x) , P ( x) ) ) , implies ( P ( x) , P ( x) ) ) ) , implies (implies ( a, implies ( b, c) ) , implies (implies ( a, b) , implies ( a, c) ) ) ) , axiom_instance (implies ( P ( x) , implies (implies ( P ( x) , P ( x) ) , P ( x) ) ) , implies ( a, implies ( b, a) ) ) , ModusPonens (implies (implies ( P ( x) , implies ( P ( x) , P ( x) ) ) , implies ( P ( x) , P ( x) ) ) , 2 , 1 ) , axiom_instance (implies ( P ( x) , implies ( P ( x) , P ( x) ) ) , implies ( a, implies ( b, a) ) ) , ModusPonens (implies ( P ( x) , P ( x) ) , 4 , 3 ) ) ) , Generalisation (forall [ x ] . (implies ( P ( x) , P ( x) ) ) , 5 ) )

Popcorn

logic3.complete_pred_theorem(quant1.forall[$x -> $P($x) ==> $P($x)], logic3.proof([logic3.axiom_instance($P($x) ==> $P($x) ==> $P($x) ==> $P($x) ==> $P($x) ==> $P($x) ==> $P($x) ==> $P($x) ==> $P($x), $a ==> $b ==> $c ==> $a ==> $b ==> $a ==> $c) , logic3.axiom_instance($P($x) ==> $P($x) ==> $P($x) ==> $P($x), $a ==> $b ==> $a) , logic3.ModusPonens($P($x) ==> $P($x) ==> $P($x) ==> $P($x) ==> $P($x), 2, 1) , logic3.axiom_instance($P($x) ==> $P($x) ==> $P($x), $a ==> $b ==> $a) , logic3.ModusPonens($P($x) ==> $P($x), 4, 3)]), logic3.Generalisation(quant1.forall[$x -> $P($x) ==> $P($x)], 5))

Rendered Presentation MathML

$$\mathrm{complete\_pred\_theorem}(\forall \hspace{0.17em}x.P\left(x\right)\Rightarrow P\left(x\right),\mathrm{proof}\left(\begin{array}{c}\mathrm{axiom\_instance}(P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right),a\Rightarrow b\Rightarrow c\Rightarrow a\Rightarrow b\Rightarrow a\Rightarrow c)\hfill \\ \mathrm{axiom\_instance}(P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right),a\Rightarrow b\Rightarrow a)\hfill \\ \mathrm{ModusPonens}(P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right),2,1)\hfill \\ \mathrm{axiom\_instance}(P\left(x\right)\Rightarrow P\left(x\right)\Rightarrow P\left(x\right),a\Rightarrow b\Rightarrow a)\hfill \\ \mathrm{ModusPonens}(P\left(x\right)\Rightarrow P\left(x\right),4,3)\hfill \end{array}\right),\mathrm{Generalisation}(\forall \hspace{0.17em}x.P\left(x\right)\Rightarrow P\left(x\right),5))$$

Signatures:

sts

---

[Next: prop_deduction] [Previous: complete_prop_theorem] [Top]

---

prop_deduction

Description:

This symbol is used to claim that a statement (the first child) is a deduction of the classical propositional calculus, i.e. that it follows by applications of Modus Ponens from instantiations of the axioms (which may be the common three involving 'implies', but need not be), and the hypotheses (elements of the set which is the second child).

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
  <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMS name="prop_theorem" cd="logic3"/>
      <OMV name="T"/>
    </OMA>
    <OMA>
      <OMS name="prop_deduction" cd="logic3"/>
      <OMV name="T"/>
      <OMS name="emptyset" cd="set1"/>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="logic3">prop_theorem</csymbol><ci>T</ci></apply>
  <apply><csymbol cd="logic3">prop_deduction</csymbol><ci>T</ci><csymbol cd="set1">emptyset</csymbol></apply>
 </apply>
</math>

Prefix

eq (prop_theorem ( T) , prop_deduction ( T, emptyset) )

Popcorn

logic3.prop_theorem($T) = logic3.prop_deduction($T, set1.emptyset)

Rendered Presentation MathML

$$\mathrm{prop\_theorem}\left(T\right)=\mathrm{prop\_deduction}(T,\varnothing )$$

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="prop_deduction"/>
    <OMV name="A"/>
    <OMA>
      <OMS cd="set1" name="set"/>
      <OMV name="A"/>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">prop_deduction</csymbol>
  <ci>A</ci>
  <apply><csymbol cd="set1">set</csymbol><ci>A</ci></apply>
 </apply>
</math>

Prefix

prop_deduction ( A, set ( A) )

Popcorn

logic3.prop_deduction($A, {$A})

Rendered Presentation MathML

$$\mathrm{prop\_deduction}(A,\left\{A\right\})$$

Signatures:

sts

---

[Next: complete_prop_deduction] [Previous: complete_pred_theorem] [Top]

---

complete_prop_deduction

Description:

This symbol is used to claim, with proof (the third child), that a statement (the first child) is a deduction of the classical propositional calculus, i.e. that it follows by applications of Modus Ponens from instantiations of the axioms (which may be the common three involving 'implies', but need not be), and the hypotheses (elements of the set which is the second child).

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS name="complete_prop_deduction" cd="logic3"/>
  <OMV name="a"/>
  <OMA>
    <OMS name="set" cd="set1"/>
    <OMV name="a"/>
  </OMA>
  <OMA>
    <OMS name="proof" cd="logic3"/>
    <OMA>
      <OMS name="list" cd="list1"/>
      <OMA>
        <OMS name="Hypothesis" cd="logic3"/>
        <OMV name="a"/>
      </OMA>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">complete_prop_deduction</csymbol>
  <ci>a</ci>
  <apply><csymbol cd="set1">set</csymbol><ci>a</ci></apply>
  <apply><csymbol cd="logic3">proof</csymbol>
   <apply><csymbol cd="list1">list</csymbol>
    <apply><csymbol cd="logic3">Hypothesis</csymbol><ci>a</ci></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

complete_prop_deduction ( a, set ( a) , proof (list (Hypothesis ( a) ) ) )

Popcorn

logic3.complete_prop_deduction($a, {$a}, logic3.proof([logic3.Hypothesis($a)]))

Rendered Presentation MathML

$$\mathrm{complete\_prop\_deduction}(a,\left\{a\right\},\mathrm{proof}\left(\left(\mathrm{Hypothesis}\left(a\right)\right)\right))$$

Signatures:

sts

---

[Next: pred_deduction] [Previous: prop_deduction] [Top]

---

pred_deduction

Description:

This symbol is used to claim that a statement (the first child) is a deduction of the classical predicate calculus, i.e. that it follows by applications of Modus Ponens, forall-introduction and exists-elimination, from instantiations of the axioms (which may be the common three involving applications of Modus Ponens, and generalisation from instantiations of the Axioms (which may be the common three involving 'implies', together with forall-instantiation and moving forall inside implication, but need not be), and the hypotheses (elements of the set which is the second child).

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
  <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMS name="pred_theorem" cd="logic3"/>
      <OMV name="T"/>
    </OMA>
    <OMA>
      <OMS name="pred_deduction" cd="logic3"/>
      <OMV name="T"/>
      <OMS name="emptyset" cd="set1"/>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="logic3">pred_theorem</csymbol><ci>T</ci></apply>
  <apply><csymbol cd="logic3">pred_deduction</csymbol><ci>T</ci><csymbol cd="set1">emptyset</csymbol></apply>
 </apply>
</math>

Prefix

eq (pred_theorem ( T) , pred_deduction ( T, emptyset) )

Popcorn

logic3.pred_theorem($T) = logic3.pred_deduction($T, set1.emptyset)

Rendered Presentation MathML

$$\mathrm{pred\_theorem}\left(T\right)=\mathrm{pred\_deduction}(T,\varnothing )$$

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic3" name="pred_deduction"/>
    <OMA>
      <OMV name="P"/>
      <OMV name="x"/>
    </OMA>
    <OMA>
      <OMS cd="set1" name="set"/>
      <OMA>
        <OMV name="P"/>
        <OMV name="x"/>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic3">pred_deduction</csymbol>
  <apply><ci>P</ci><ci>x</ci></apply>
  <apply><csymbol cd="set1">set</csymbol><apply><ci>P</ci><ci>x</ci></apply></apply>
 </apply>
</math>

Prefix

pred_deduction ( P ( x) , set ( P ( x) ) )

Popcorn

logic3.pred_deduction($P($x), {$P($x)})

Rendered Presentation MathML

$$\mathrm{pred\_deduction}(P\left(x\right),\left\{P\left(x\right)\right\})$$

Signatures:

sts

---

[Next: complete_pred_deduction] [Previous: complete_prop_deduction] [Top]

---

complete_pred_deduction

Description:

This symbol is used to claim, with proof (the third child), that a statement (the first child) is a deduction of the classical predicate calculus, i.e. that it follows by applications of Modus Ponens, forall-introduction and exists-elimination, from instantiations of the axioms (which may be the common three involving applications of Modus Ponens, and generalisation from instantiations of the Axioms (which may be the common three involving 'implies', together with forall-instantiation and moving forall inside implication, but need not be), and the hypotheses (elements of the set which is the second child).

Signatures:

sts

---

[Next: is_deduction] [Previous: pred_deduction] [Top]

---

is_deduction

Description:

This symbol expresses whether or not there is a deduction of the form quoted. Hence for items of type complete_pred_deduction, it is always true

The Deduction Theorem (of propositional calculus).

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS name="implies" cd="logic1"/>
  <OMA>
    <OMS name="is_deduction" cd="logic3"/>
    <OMA>
      <OMS name="prop_deduction" cd="logic3"/>
      <OMV name="P"/>
      <OMA>
        <OMS name="set" cd="set1"/>
        <OMV name="H"/>
      </OMA>
    </OMA>
  </OMA>
  <OMA>
    <OMS name="is_theorem" cd="logic3"/>
    <OMA>
      <OMS name="prop_theorem" cd="logic3"/>
      <OMA>
        <OMS name="implies" cd="logic1"/>
        <OMV name="H"/>
        <OMV name="P"/>
      </OMA>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="logic3">is_deduction</csymbol>
   <apply><csymbol cd="logic3">prop_deduction</csymbol>
    <ci>P</ci>
    <apply><csymbol cd="set1">set</csymbol><ci>H</ci></apply>
   </apply>
  </apply>
  <apply><csymbol cd="logic3">is_theorem</csymbol>
   <apply><csymbol cd="logic3">prop_theorem</csymbol>
    <apply><csymbol cd="logic1">implies</csymbol><ci>H</ci><ci>P</ci></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

implies (is_deduction (prop_deduction ( P, set ( H) ) ) , is_theorem (prop_theorem (implies ( H, P) ) ) )

Popcorn

logic3.is_deduction(logic3.prop_deduction($P, {$H})) ==> logic3.is_theorem(logic3.prop_theorem($H ==> $P))

Rendered Presentation MathML

$$\mathrm{is\_deduction}\left(\mathrm{prop\_deduction}(P,\left\{H\right\})\right)\Rightarrow \mathrm{is\_theorem}\left(\mathrm{prop\_theorem}\left(H\Rightarrow P\right)\right)$$

Signatures:

sts

---

[First: prop_theorem] [Previous: complete_pred_deduction] [Top]