% $Id: FormalSystem.lsl,v 1.4 2003/10/01 07:25:52 connolly Exp$ % A transcription of % %html Formal Systems - Definitions % (from Ruth E. Davis, Truth, Deduction, and Computation. % New York: Computer Science press, 1989.) % % (c) Charles F. Schmidt % Last Modified: Saturday, May 08, 1999 9:07:08 PM GMT FormalSystem: trait includes CoerceContainer(List[Formula], FiniteSet[Formula], Formula for E), RelSet(Formula, Set[Formula]), Set(Formula, FiniteSet[Formula] for Set[E]), Set(Rule, FiniteSet[Rule] for Set[E]), List(Formula), Relation(Formula, Rel[Formula]) introduces % do this as a tuple? wff: System, Formula -> Bool wff: System, Set[Formula] -> Bool axiom: System, Formula -> Bool rules: System -> FiniteSet[Rule] negation: System, Formula -> Formula arity: Rule -> Int % positive direct_consequence: System, Rule, FiniteSet[Formula], Formula -> Bool % for direct_consequence(T, Ri, S, A) read % A is a direct consequence of S by virtue of Ri in T. deducible: System, Set[Formula], Formula -> Bool % for deducible(T, S, P) read P is deducible from S in T. proof: System, Set[Formula], Formula, List[Formula] -> Bool % for proof(T, S, P, Pi) read Pi is a proof of P from S in T. theorem: System, Formula -> Bool % for theorem(T, P) read P is a theorem (or: is provable) in T interpret: System, Interpretation, Formula -> Bool model: System, Interpretation, Set[Formula] -> Bool complete: System -> Bool sound: System -> Bool consistent: System -> Bool %@@compactness, etc. asserts \forall T: System, Ri: Rule, S: Set[Formula], A, f, P: Formula, Sf: FiniteSet[Formula], Pi: List[Formula] wff(T, S) /\ f \in S => wff(T, f); %@@ do we need the only if rule? arity(Ri) > 0; axiom(T, A) => wff(T, A); direct_consequence(T, Ri, Sf, A) => size(Sf) = arity(Ri); direct_consequence(T, Ri, Sf, A) /\ f \in Sf => wff(T, f); proof(T, S, P, Pi) = ( (last(Pi) = P) /\ (axiom(T, P) \/ P \in S \/ \E Ri \E Sf (Ri \in rules(T) /\ Sf \subset coerce(Pi) /\ direct_consequence(T, Ri, Sf, P) /\ (init(Pi) = empty \/ proof(T, S, last(init(Pi)), init(Pi)) ) ) ) ); deducible(T, S, P) = \E Pi (proof(T, S, P, Pi)); theorem(T, P) = deducible(T, {}, P); \forall T: System, I: Interpretation, S: Set[Formula], f: Formula, Pi: List[Formula] interpret(T, I, f) => wff(T, f); model(T, I, S) = \A f (wff(T, f) /\ f \in S => interpret(T, I, f)); complete(T) = \A f ( (\A I interpret(T, I, f)) => theorem(T, f) ); sound(T) = \A f ( theorem(T, f) => (\A I interpret(T, I, f))); consistent(T) = \not \E f ( theorem(T, f) /\ theorem(T, negation(T, f))); implies \forall S1, S2: Set[Formula], A: Formula, T: System % monotonicity wff(T, S1) /\ wff(T, S2) /\ wff(T, A) => (S1 \subset S2 /\ deducible(T, S1, A) => deducible(T, S2, A)); %@@compactness, etc.