A new piece of math notation I’ve invented which I plan to use whenever I am writing proofs for myself (rather than for other people).
Sometimes when writing a proof, for some long property P(x) I want to write:
It follows from foo, that there exists x such that P(x). Let x be such that P(x). Then …
I don’t like that I need to write P(x) twice here. And the whole construction is too long for my liking, especially when the reason foo why such x exists is obvious. And if I omit the first sentence It follows from foo, that there exists x such that P(x). and just write
Let x be such that P(x). Then …
then it’s not clear what I mean. It could be that I want to show that such x exists and that from its existence some statement of interest follows. Or it could be that I want to prove some statement of form
For each x such that P(x), it holds that Q(x).
Or it could even be that I want to show that something follows from existence of such x, but I am not asserting that such x exists.
The new notation I came up with is to write L∃t in cases when I want to assert that such x exists and to bound the variable x in the same place. An example (an excerpt, not a complete proof):
Suppose D is a countably infinite set, suppose S is a set of subsets of D, suppose X∈S.
L∃t b be a bijection from N onto D.
L∃t step:S→S such that ∀Y∈Sstep(Y)=Y, if Y is ⊆-maximal in S, otherwise step(Y)=Y∪{b(min({n∈N∣b(n)∉Y∧Y∪{b(n)}∈S}))}.
By recursion theorem, L∃t ⟨Xn∣n∈N⟩ be such that X0=X, ∀n≥1Xn=step(Xn−1).
A new piece of math notation I’ve invented which I plan to use whenever I am writing proofs for myself (rather than for other people).
Sometimes when writing a proof, for some long property P(x) I want to write:
It follows from foo, that there exists x such that P(x). Let x be such that P(x). Then …
I don’t like that I need to write P(x) twice here. And the whole construction is too long for my liking, especially when the reason foo why such x exists is obvious. And if I omit the first sentence It follows from foo, that there exists x such that P(x). and just write
Let x be such that P(x). Then …
then it’s not clear what I mean. It could be that I want to show that such x exists and that from its existence some statement of interest follows. Or it could be that I want to prove some statement of form
For each x such that P(x), it holds that Q(x).
Or it could even be that I want to show that something follows from existence of such x, but I am not asserting that such x exists.
The new notation I came up with is to write L∃t in cases when I want to assert that such x exists and to bound the variable x in the same place. An example (an excerpt, not a complete proof):
Suppose D is a countably infinite set, suppose S is a set of subsets of D, suppose X∈S.
L∃t b be a bijection from N onto D.
L∃t step:S→S such that ∀Y∈S step(Y)=Y, if Y is ⊆-maximal in S, otherwise step(Y)=Y∪{b(min({n∈N∣b(n)∉Y∧Y∪{b(n)}∈S}))}.
By recursion theorem, L∃t ⟨Xn∣n∈N⟩ be such that X0=X, ∀n≥1 Xn=step(Xn−1).
L∃t M=⋃n∈NXn.
...