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:
axiom_instance, complete_pred_deduction, complete_pred_theorem, complete_prop_deduction, complete_prop_theorem, Generalisation, hypothesis, is_deduction, is_theorem, ModusPonens, pred_deduction, pred_theorem, proof, prop_deduction, prop_theorem
Date:
2001-07-31
Version:
0 (Revision 1)
Review Date:
2003-09-01
Status:
experimental
Uses CD:
alg1, arith1, fns1, list1, logic1, quant1, relation1, set1

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

prop_theorem

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: 
<OMOBJ>
  <OMA>
    <OMS cd="logic3" name="prop_theorem"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="A"/>
      <OMV name="A"/>
    </OMA>
  </OMA>
</OMOBJ>

prop_theorem (implies ( A, A) )

Signatures:
sts

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

pred_theorem

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: 
<OMOBJ>
  <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>

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

Signatures:
sts

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

is_theorem

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

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: 
<OMOBJ>
<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>

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

Example: 
<OMOBJ>
<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>

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

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: 
<OMOBJ>
<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="relations1"/>
          <OMV name="x"/>
          <OMS name="zero" cd="alg1"/>
        </OMA>
        <OMA>
          <OMS name="eq" cd="relations1"/>
          <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="relations1"/>
        <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="relations1"/>
        <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>

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

Signatures:
sts

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

ModusPonens

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: 
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="ModusPonens"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="a"/>
      <OMV name="a"/>
    </OMA>
    <OMI> 4 </OMI>
    <OMI> 2 </OMI>
  </OMA>
</OMOBJ>

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

Signatures:
sts

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

Generalisation

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: 
<OMOBJ>
  <OMA>
    <OMS cd="logic1" 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>

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

Signatures:
sts

[Next: hypothesis] [Previous: ModusPonens] [Top]

hypothesis

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

Example: 
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="Hypothesis"/>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMV name="a"/>
      <OMV name="a"/>
    </OMA>
  </OMA>
</OMOBJ>

Hypothesis (implies ( a, a) )

Signatures:
sts

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

proof

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: 
<OMOBJ>
  <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>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>

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

Signatures:
sts

[Next: complete_prop_theorem] [Previous: hypothesis] [Top]

complete_prop_theorem

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: 
<OMOBJ>
  <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>
        </OMA>
      </OMA>
    </OMA> 
  </OMA>
</OMOBJ>

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

Signatures:
sts

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

complete_pred_theorem

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: 
<OMOBJ>
  <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>
        </OMA>
      </OMA>
    </OMA> 
    <OMA>
      <OMS cd="logic1" 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>

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) ) ) ) ) , Generalisation (forall [ x ] . (implies ( P ( x) , P ( x) ) ) , 5 ) )

Signatures:
sts

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

prop_deduction

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): 
<OMOBJ>
  <OMA>
  <OMS name="eq" cd="relations1"/>
    <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>

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

Example: 
<OMOBJ>
  <OMA>
    <OMS cd="logic3" name="prop_deduction"/>
    <OMV name="A"/>
    <OMA>
      <OMS cd="set1" name="set"/>
      <OMV name="A"/>
    </OMA>
  </OMA>
</OMOBJ>

prop_deduction ( A, set ( A) )

Signatures:
sts

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

complete_prop_deduction

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: 
<OMOBJ>
<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>

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

Signatures:
sts

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

pred_deduction

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): 
<OMOBJ>
  <OMA>
  <OMS name="eq" cd="relations1"/>
    <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>

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

Example: 
<OMOBJ>
  <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>

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

Signatures:
sts

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

complete_pred_deduction

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

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: 
<OMOBJ>
<OMA>
  <OMS name="implies" cd="logic1"/>
  <OMA>
    <OMS name="is_deduction" cd="logic3"/>
    <OMA>
      <OMS name="prop_deduction"/>
      <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"/>
      <OMA>
        <OMS name="implies" cd="logic1"/>
        <OMV name="H"/>
        <OMV name="P"/>
      </OMA>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

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

Signatures:
sts

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