% $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.