# Creative Commons Attribution-Share Alike 3.0 Unported (http://creativecommons.org/licenses/by-sa/3.0/)
# {{header
# | title = Axioms of quantifiability
# | subtitle =
# | left =
# | right =
# | shortcut =
# | notes = The axiom of quantifiability asserts that any object (term) can be made equal to a variable which is subject to quantification. It corresponds roughly to the notion that there are no [[w:proper class|proper classes]].
# }}
#
# In [[Interface:First-order logic]], we present a theory which deals with quantifiers (∀ and ∃), free variables, and the substitution of one variable for another. However, there is an issue with substitution of a term for a variable. To make this work as straightforwardly as substitution of a variable for a variable, we put forth an axiom here which we call the axiom of quantifiability. It is a variant of the axiom of existence which says that we can introduce a variable equal to a given variable.
#
# == Prerequisities ==
# We build on [[Interface:Classical propositional calculus]] and [[Interface:First-order logic]]:
param (CLASSICAL Classical_propositional_calculus.ghi () "")
param (FIRSTORDER First-order_logic.ghi (CLASSICAL) "")
#
# == Equality between terms ==
# The axiom of quantifiability is all about equality between terms, not just equality between variables. At least for now, First-order_logic.ghi defines equality between terms, so we don't need to do anything here.
#
# == The axiom of quantifiability ==
#
# The axiom:
#
var (object x)
tvar (object s)
stmt (Quantifiability ((s x)) () (∃ x (= x s)) )
#
# == Consequences ==
# In some formulations of [[w:set theory|set theory]], for example metamath's set.mm, a variable (something which can be quantified over) corresponds to a set, and an object corresponds to a class.
#
# As can be seen in more detail in [[First-order logic with quantifiability]] and [[Interface:First-order logic with quantifiability]], the axiom of quantifiability allows substitution of a term for a variable. In metamath's set.mm, such substitution is still possible, but it requires an additional hypothesis. For example, set.mm's `vtocl`

has as a hypothesis `A ∈ V`

which means "A is not a proper class".[[http://us.metamath.org/mpeuni/vtocl.html vtocl] in metamath's set.mm, accessed May 6, 2010]
#
# First-order logic with quantifiability works fine for Peano arithmetic (see for example Raph Levien's peano_thms[[http://levien.com/garden/ghnew/peano/ Peano], accessed 6 May 2010]), and set theories without proper classes, such as ZF.
#
# == Similar axioms/theorems in other systems ==
# Metamath's set.mm has a theorem `A ∈ B → ∃ x x = A`

(where `A`

and `B`

are classes and `x`

is a variable),[[http://us.metamath.org/mpeuni/elex.html elex], accessed 31 May 2010] which closely resembles our axiom of quantifiability except for A ∈ B (which means "A is not a proper class").
#
# == References ==
#
#
# [[Category:Classical first-order logic|{{PAGENAME}}]]