An infinite number of axioms like in an axiom schema doesn’t really hurt anything, but you can’t have infinitely long single axioms.
∀x((x = 0) ∨ (x = S0) ∨ (x = SS0) ∨ (x = SSS0) ∨ ...)
is not an option. And neither is the axiom set
P0(x) iff x = 0 PS0(x) iff x = S0 PSS0(x) iff x = SS0 ... ∀x(P0(x) ∨ PS0(x) ∨ PS0(x) ∨ PS0(x) ∨ ...)
We could instead try the axioms
P(0, x) iff x = 0 P(S0, x) iff x = S0 P(SS0, x) iff x = SS0 ... ∀x(∃n(P(n, x)))
but then again we have the problem of n being a nonstandard number.
Current theme: default
Less Wrong (text)
Less Wrong (link)
Arrow keys: Next/previous image
Escape or click: Hide zoomed image
Space bar: Reset image size & position
Scroll to zoom in/out
(When zoomed in, drag to pan; double-click to close)
Keys shown in yellow (e.g., ]) are accesskeys, and require a browser-specific modifier key (or keys).
]
Keys shown in grey (e.g., ?) do not require any modifier keys.
?
Esc
h
f
a
m
v
c
r
q
t
u
o
,
.
/
s
n
e
;
Enter
[
\
k
i
l
=
-
0
′
1
2
3
4
5
6
7
8
9
→
↓
←
↑
Space
x
z
`
g
An infinite number of axioms like in an axiom schema doesn’t really hurt anything, but you can’t have infinitely long single axioms.
is not an option. And neither is the axiom set
We could instead try the axioms
but then again we have the problem of n being a nonstandard number.