git @ Cat's Eye Technologies Maxixe / 4cd2628
Try to justify the presence/absence of 'unique' attribute. Chris Pressey 8 years ago
1 changed file(s) with 39 addition(s) and 19 deletion(s). Raw diff Collapse all Expand all
+39
-19
doc/Examples.md less more
132132 of a turnstile can be filled out by a variable on the LHS, so I've taken the liberty of turning
133133 it into a rule.
134134
135 The atom introduced as the variable in the `forall` must be unique (i.e. not used previously in
136 the proof.) This implements scope. Without that restriction, it is possible to confuse
137 arbitrary and particular variables and write proofs that make no sense.
135 The variable being introduced by Universal Generalization need not be unique, because it
136 is bound in a `forall`.
137
138 Note that the substitution operation `P[X -> V]` used in the Universal Generalization rule
139 first checks that the instance of V does not already occur in P.
140
141 (This may in fact be overly restrictive. But it seems like the most hardship it causes at
142 the moment is that it requires you to select different names for variables in parts of the
143 proof. For example, below we show a result `forall(y, ...)`. We could just as easily
144 want to show the result `forall(x, ...)` but x is already a free (arbitrary) variable in
145 this proof.)
138146
139147 We use `c(zero)` to represent zero because we can't use `zero` because then you could use it as
140148 a variable name and say something silly like `forall(zero, ...)`.
143151 Premise = |- eq(add(x, c(zero)), x)
144152 Commutivity_of_Equality = eq(E1, E0) |- impl(eq(E1, E0), eq(E0, E1))
145153 Modus_Ponens = P0 ; impl(P0, P1) |- P1
146 Universal_Generalization = P ; X{term} ; V{unique atom} |- forall(V, P[X -> V])
154 Universal_Generalization = P ; X{term} ; V{atom} |- forall(V, P[X -> V])
147155 show
148156 forall(y, eq(y, add(y, c(zero))))
149157 proof
158166
159167 All bugs are creepy and all bugs are crawly therefore all bugs are both creepy and crawly.
160168
161 Note that the term introduced as the variable in the UI need *not* be unique, because if
169 Note that the term introduced as the variable in the UI need not be unique, because if
162170 something is true for all `x`, it is true for *all* `x`, even if `x` is something else
163 you've already been thinking about and given the name `x`.
164
165 Note that it also need not be an atom.
171 you've already been thinking about and given the name `x`. Note that it also need not
172 be an atom.
173
174 Note that the substitution operation `P[X -> V]` used in the Universal Instantiation rule
175 first checks that the instance of V does not already occur in P. This prevents situations
176 like instantiating ∀x.∃y.x≠y with y, to obtain ∃y.y≠y.
166177
167178 given
168179 Modus_Ponens = impl(P, Q) ; P |- Q
174185 end
175186 end
176187
177 Universal_Generalization = P ; X{term} ; V{unique atom} |- forall(V, P[X -> V])
188 Universal_Generalization = P ; X{term} ; V{atom} |- forall(V, P[X -> V])
178189 Universal_Instantiation = forall(X, P) ; V{term} |- P[X -> V]
179190
180191 Premise_1 = |- forall(x, impl(bug(x), creepy(x)))
203214
204215 All bugs are creepy therefore there exists a bug which is creepy.
205216
206 Again, the new variable name introduced into the `exists` must be unique to avoid
207 scope problems.
217 The variable being introduced by Existential Generalization need not be unique, because it
218 is bound in an `exists`.
219
220 Like always with `[X -> V]`, an occurs check occurs. Not sure if necessary atm.
208221
209222 given
210223 Universal_Instantiation = forall(X, P) ; V{term} |- P[X -> V]
211 Existential_Generalization = P ; X{term} ; V{unique atom} |- exists(V, P[X -> V])
224 Existential_Generalization = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
212225
213226 Premise = |- forall(x, impl(bug(x), creepy(x)))
214227 show
225238 All men are mortal. There exists a man named Socrates. Therefore there exists a man who is mortal
226239 and who is named Socrates.
227240
228 Very unlike UI, the new variable name introduced during EI needs to be both unique to avoid
229 scope problems, and local, to prevent the name from "leaking out" of the EI block.
241 Very unlike UI, to avoid scoping problems, the new variable name introduced during EI needs to be:
242
243 * an atom, because instantiating an entire term is probably unjustifiable sometimes
244 * unique, to avoid clashing with another variable that was previously instantiated
245 * local, to prevent the name from "leaking out" of the EI block.
246
247 Note that the substitution operation `P[X -> V]` used in the Existential Instantiation rule
248 first checks that the instance of V does not already occur in P. This prevents situations
249 like instantiating ∃x.∀y.p(y)→x≠y with y, to obtain ∀y.p(y)→y≠y.
230250
231251 given
232252 Modus_Ponens = impl(P, Q) ; P |- Q
236256 Tautology = P |- P
237257
238258 Universal_Instantiation = forall(X, P) ; V{term} |- P[X -> V]
239 Existential_Generalization = P ; X{term} ; V{unique atom} |- exists(V, P[X -> V])
259 Existential_Generalization = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
240260 block Existential_Instantiation
241261 case
242262 Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
268288 For comparison, here are all of the rules for Universal (resp. Existential)
269289 Generalization (resp. Instantiation) shown together in one place, with abbreviated names:
270290
271 UG = P ; X{term} ; V{unique atom} |- forall(V, P[X -> V])
291 UG = P ; X{term} ; V{atom} |- forall(V, P[X -> V])
272292 UI = forall(X, P) ; V{term} |- P[X -> V]
273 EG = P ; X{term} ; V{unique atom} |- exists(V, P[X -> V])
293 EG = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
274294 block EI
275295 case
276296 Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
315335 As long as it's not the same as any atom already in P. (This sounds familiar.)
316336
317337 given
318 UG = P ; X{term} ; V{unique atom} |- forall(V, P[X -> V])
338 UG = P ; X{term} ; V{atom} |- forall(V, P[X -> V])
319339 UI = forall(X, P) ; V{term} |- P[X -> V]
320 EG = P ; X{term} ; V{unique atom} |- exists(V, P[X -> V])
340 EG = P ; X{term} ; V{atom} |- exists(V, P[X -> V])
321341 block EI
322342 case
323343 Let = exists(X, P) ; V{unique local atom} |- P[X -> V]