blob: b4281734951a9ba2740a3da14f20fa9ce1392701 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
%%%
%%% Example script for Twelf Proof General.
%%%
%%% $Id$
%%%
%%% Rather than a proof this file is just a signature,
%%% bunch of declarations. Would be nice to have something
%%% closer to other systems for pedagogical purposes...
%%% (i.e. proving commutativity of conjunction in ND fragment
%%% of this logic)
%%% Intuitionistic propositional calculus
%%% Positive fragment with implies, and, true.
%%% Two formulations here: natural deduction and Hilbert-style system.
%%% Author: Frank Pfenning
% Type of propositions.
o : type.
%name o A.
% Syntax: implication, plus a few constants.
=> : o -> o -> o. %infix right 10 =>.
& : o -> o -> o. %infix right 11 &.
true : o.
% Provability.
|- : o -> type. %prefix 9 |-.
%name |- P.
% Axioms.
K : |- A => B => A.
S : |- (A => B => C) => (A => B) => A => C.
ONE : |- true.
PAIR : |- A => B => A & B.
LEFT : |- A & B => A.
RIGHT : |- A & B => B.
% Inference Rule.
MP : |- A => B -> |- A -> |- B.
% Natural Deduction.
! : o -> type. %prefix 9 !.
%name ! D.
trueI : ! true.
andI : ! A -> ! B -> ! A & B.
andEL : ! A & B -> ! A.
andER : ! A & B -> ! B.
impliesI : (! A -> ! B) -> ! A => B.
impliesE : ! A => B -> ! A -> ! B.
% Normal deductions (for faster search)
!^ : o -> type.
!v : o -> type.
trueI^ : !^ true.
andI^ : !^ A -> !^ B -> !^ (A & B).
andEvL : !v (A & B) -> !v A.
andEvR : !v (A & B) -> !v B.
impI^ : (!v A -> !^ B) -> !^ (A => B).
impEv : !v (A => B) -> !^ A -> !v B.
close : !v A -> !^ A.
|
