logic3 http://www.openmath.org/cd/logic3.ocd 2003-09-01 2001-07-31 0 1 experimental 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). 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). 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 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. 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. 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. 4 2 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. 5 Hypothesis This symbol represents that a wellformed formula is a hypothesis of a deduction of the propositional or predicate calculus. 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. 2 1 4 3 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). 2 1 4 3 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). 2 1 4 3 5 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). 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). 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). 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). 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).