Does Jow Forums prove theorems?

Does Jow Forums prove theorems?

Attached: serveimage.png (802x481, 73K)

Other urls found in this thread:

leanprover.github.io/theorem_proving_in_lean/
adam.chlipala.net/cpdt/
youtube.com/watch?v=bTLc_9buWLQ
home.sandiego.edu/~shulman/papers/trinity.pdf#page=23
twitter.com/NSFWRedditGif

Proof of Lemma

Let us define a model N = (λ, RN ) by: RN = {(α0, . . . , αk) : αi < λ and i1 < i2 ≤ k = αi1 6= αi2 mod n and i1 < i2 ≤ k = (∃β)(αi1 < nβ ≤ αi2 ∨ αi2 < nβ ≤ αi1 )}. By definition RN is irreflexive, symmetric, and (k + 1)-ary. Let us first show that if w ∈ [λ] n+1 then w is not a complete RN-hypergraph. If |w| = n + 1, for some α1 6= α2 ∈ w we have α1 = α2 mod n. Choose v ⊆ w such that α1 ∈ v, α2 ∈ v, and |v| = k + 1. Then by definition R cannot hold on {α : α ∈ v}, so w cannot be a complete R-hypergraph. So N is a submodel of some N0 |= Tn,k of cardinality λ.
Second, let us show that if F : [λ] k [λ] we have (β < nγ + n) ∧ (γ < nβ + n)
>and γ ∈ F({nα0 + i0, . . . , nαk−1 + ik−1})}

As we have assumed (λ, k, µ) n, there is w1 = {α ∗ i : i < n} such that α ∗ 0 < · · · < α∗ n−1 < λ and for all v ∈ [n] k , w1 6⊆ F1({α ∗ : ∈ v}). Define βi = nα∗ i + i for i < n and let w2 = {βi : i < n}, and let us show w2 is as required for F. First, trivially |w2| = n, as |w1| = n. Second, by definition of RN above, w2 is a complete RN-hypergraph. Third, let us show that if u ∈ [w2] k and w2 ⊆ F(u) then we get a contradiction. Let v ∈ [n] k be such that u = {βi : i ∈ v}. Then u1 := {α ∗ i : i ∈ v} ∈ [w1] k and w1 ⊆ F(u1). [This is because for each α ∗ i , i < n we presently have βi ∈ F(u) so there is an element

>γ ∈ F({nα∗ 0 + 0, . . . , nα∗ k−1 + (k − 1)}) = F(β0, . . . , βk−1)

(1/2)

(2/2)

such that (α ∗ i < nγ + n) ∧ (γ < nα∗ i + n), namely γ = βi , which belongs to F(β0, . . . , βk−1) since F is a strong set mapping. This contradicts the choice of w1. We have shown that for all u ∈ [w2] k , w2 6⊆ F(u), so w2 is as required which completes the proof.

What are you proving here user?

Teach me how

Yes but not with a computer, there is no general algorithm for proving a theorem and Gödel said its impossible anyway. I do it by hand.

While Gödel's theorems do say that there are true theorems which cannot be proved in a sufficiently strong axiomatic theory, this has nothing to do with formal proofs.

A formal proof is orders of magnitude more trustworthy than a conventional handwritten proof.

leanprover.github.io/theorem_proving_in_lean/

that he can do something you can't. proofs are pointless irl. closest thing to them is static testing of kode.

Do you have some resources on coq?
I want to get started but I can't into the syntax and basic approach for getting things done.

I want to read convex optimization papers andet the machine do the math to verify the bounds are correct.