blob: 663592f713af49a3878803d17de9a43320dbc60f (
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
|
param (PROP-MIN prop-min.ghi () "")
param (PROP-EXT prop-ext.ghi (PROP-MIN) "")
kind (set)
var (wff ph ps ch th ta)
var (set x y z w v u)
term (wff (A. set wff))
# We comment out some older versions of axioms 5 and 6.
# stmt (ax-5 () () ((-> (A. x (-> (A. x ph) ps)) (-> (A. x ph) (A. x ps)))))
# stmt (ax-6 () () ((-> (-. (A. x (-. (A. x ph)))) ph)))
# Axioms ax-5, ax-6, ax-7, ax-gen, and ax-17 are all consistent
# with an interpretation in which (A. x ph) evaluates to True
# regardless of ph and x. That's obviously not the interpretation
# of (A. x ph) that we want. Metamath does not include ax-4 among
# its axioms of predicate logic, but its proof ax4 in Metamath requires
# the axioms concerning equality, which we do not introduce yet.
# (Specifically, the Axiom of Existence, (-. (A. x (-. (= (cv x) (cv y)))))
# is inconsistent with the above interpretation.)
# So, we keep ax-4 here.
# Axiom of Specialization
stmt (ax-4 () () ((-> (A. x ph) ph)))
# Axiom of Quantified Implication
stmt (ax-5 () () ((-> (A. x (-> ph ps)) (-> (A. x ph) (A. x ps)))))
# Axiom of Quantified Negation
stmt (ax-6 () () ((-> (-. (A. x ph)) (A. x (-. (A. x ph))))))
# Axiom of Quantifier Commutation
stmt (ax-7 () () ((-> (A. x (A. y ph)) (A. y (A. x ph)))))
# Rule of Generalization
stmt (ax-gen () (ph) ((A. x ph)))
# Axiom of Quantifier Introduction (2)
stmt (ax-17 ((ph x)) () ((-> ph (A. x ph))))
|
