Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > axi12  GIF version 
Description: Axiom of Quantifier
Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever z is distinct
from x and y, and x = y is
true,
then x = y quantified with z is also true. In other words, z
is irrelevant to the truth of x
= y. Axiom scheme C9' in [Megill]
p. 448 (p. 16 of the preprint). It apparently does not otherwise appear
in the literature but is easily proved from textbook predicate calculus by
cases.
An open problem is whether this axiom is redundant. Note that the analogous axiom for the membership connective, ax15 1807, has been shown to be redundant. It is also unknown whether this axiom can be replaced by a shorter formula. However, it can be derived from two slightly shorter formulas, as shown by a12study 1825. This axiom has been modified from the original ax12 1393 for compatibility with intuitionistic logic. 
Ref  Expression 

axi12  ⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y))) 
Step  Hyp  Ref  Expression 

1  vz  . . . 4 set z  
2  vx  . . . 4 set x  
3  1, 2  weq 1384  . . 3 wff z = x 
4  3, 1  wal 1335  . 2 wff ∀z z = x 
5  vy  . . . . 5 set y  
6  1, 5  weq 1384  . . . 4 wff z = y 
7  6, 1  wal 1335  . . 3 wff ∀z z = y 
8  2, 5  weq 1384  . . . . 5 wff x = y 
9  8, 1  wal 1335  . . . . 5 wff ∀z x = y 
10  8, 9  wi 4  . . . 4 wff (x = y → ∀z x = y) 
11  10, 1  wal 1335  . . 3 wff ∀z(x = y → ∀z x = y) 
12  7, 11  wo 606  . 2 wff (∀z z = y ∨ ∀z(x = y → ∀z x = y)) 
13  4, 12  wo 606  1 wff (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y → ∀z x = y))) 
Colors of variables: wff set class 
This axiom is referenced by: ax12 1393 ax12or 1394 
Copyright terms: Public domain  W3C validator 