6.7.15 Propositional calculus

Prev Up Next Page 101 of 800 Search internet

If you want to define your own theories it may be a good idea to look at the way Prop, FOL, and PA are defined. We mainly follow E. Mendelson: 'Introduction to mathematical logic' in the formulation of axioms, inference rules, and theories. To define Prop we first define axiom A1:

axiom A1 : All #x ,, #y : #x imply #y imply #x end axiom

That statement macro expands into two definitions. The first one says:

define statement of A1 as All #x : All #y : #x imply #y imply #x end define

That defines what the axiom says. It says that for all object terms #x and #y we have #x imply #y imply #x. Since implication is post-associative, the axiom says #x imply ( #y imply #x ).

The second definition reads:

define unitac of A1 as \ u . unitac-rule ( u ) end define

This defines how to prove Axiom A1: Look it up in all presently assumed theories and see it is there. If yes, generate a sequent term which extracts A1 from the theory in which it is found.

Note that looking up an axiom in all assumed theories can be costly in terms of cpu time. If you need e.g. A1 very often and always need it in a context where you have assumed e.g. PA, then prove

PA lemma "A1'" : All #x ,, #y : #x imply #y imply #x end lemma

once and for all and reference that lemma instead of axiom A1. That will save you a lot of cpu time.

Prop has more rules:

axiom A2 : All #x ,, #y ,, #z : ( #x imply #y imply #z ) imply ( #x imply #y ) imply #x imply #z end axiom

axiom A3 : All #x ,, #y : ( not #y imply not #x ) imply ( not #y imply #x ) imply #y end axiom

rule MP : All #x ,, #y : #x imply #y infer #x infer #y end rule

Axioms and rules macro expand in exactly the same way and the Logiweb sequent calculus makes absolutely no distinction between axioms and inference rules.

The understood parentheses in the MP rule are:

rule MP : All #x ,, #y : ( ( #x imply #y ) infer ( #x infer #y ) ) end rule

Thus, MP says that if we have a proof of #x imply #y then we can conclude #x infer #y. And if we also have a proof of #x then we can in turn conclude #y

The Prop defined by the Peano page also has a rule of definition:

rule Def : All #x ,, #y : def ( #x , #y ) endorse #x infer #y end rule

The rule says: For all object terms #x and #y, if the side condition def ( #x , #y ) evaluates to true then #x infer #y. The side condition def ( #x , #y ) is true if #x and #y are identical except for application of definitions.

As an example, the Peano page defines

math define x or y as not x imply y end define

In other words, the Peano page defines the 'math/kg' aspect of x or y to be not x imply y. Because of that, the Def rule allows to replace x or y by not x imply y and vice versa.

The Peano page defines the side condition def ( #x , #y ) thus:

macro define def ( a , b ) as \ c . def0 ( quote a end quote , quote b end quote , c ) end define

When the side condition is evaluated, it is applied to the cache of the page on which the proof occurs. Among other, that grants access to all definitions on that page and all transitively referenced pages. The def0 ( a , b , c ) function then traverses the terms a and b in parallel and sees if all differences are in accordance with math definitions in the cache c.

The Peano page does not follow Mendelson completely. Among other, the Peano page takes implication x imply y and falsehood ff as primitives and defines negation thus:

math define not x as x imply ff end define

The Peano page also defines truth:

math define tt as ff imply ff end define

and a couple of convenient operators like x and y, x when y, and x iff y.

The definition of Prop is a meta-conjunction:

theory Prop : A1 oplus A2 oplus A3 oplus MP oplus Def end theory

The Peano page also defines the tactic to be used on Prop proofs:

tactic define Prop as \ u . tactic-Prop ( u ) end define

That is the tactic which, among others, knows how to handle hypothetical reasoning and deduction blocks in Prop.

Prev Up Next Page 101 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05