% $Id: FormalSystem.lsl,v 1.3 2000/10/31 22:26:31 connolly Exp $
% A transcription of
%
% Formal Systems - Definitions
% (from Ruth E. Davis, Truth, Deduction, and Computation.
% New York: Computer Science press, 1989.)
% http://www-rci.rutgers.edu/~cfs/305_html/Deduction/FormalSystemDefs.html
% (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
" T: System, Ri: Rule, S: Set[Formula], A, f, P: Formula,
Sf: FiniteSet[Formula], Pi: List[Formula]
wff(T, S) Ù f Î 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 Î Sf Þ wff(T, f);
proof(T, S, P, Pi) = (
(last(Pi) = P)
Ù (axiom(T, P)
Ú P Î S
Ú $ Ri $ Sf (Ri Î 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) = $ Pi (proof(T, S, P, Pi));
theorem(T, P) = deducible(T, {}, P);
" T: System, I: Interpretation, S: Set[Formula], f: Formula,
Pi: List[Formula]
interpret(T, I, f) Þ wff(T, f);
model(T, I, S) = " f (wff(T, f) Ù f Î S Þ interpret(T, I, f));
complete(T) = " f ( (" I interpret(T, I, f))
Þ theorem(T, f) );
sound(T) = " f ( theorem(T, f) Þ (" I interpret(T, I, f)));
consistent(T) = \not $ f ( theorem(T, f) Ù theorem(T, negation(T, f)));
implies
" 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.
[Index]
[source]
HTML generated using lsl2html.