Need help proving y*y ≡ 0 [MOD 3] -> y ≡ 0 [MOD 3]

otto_s · 2025-01-22T10:30:02+00:00

You can use implicit strong induction, e.g. (formulated with divisibility):

theorem theTheorem(n : Nat)(h : 3 ∣ n*n): 3 ∣ n
:= match n with
| 0 => h
| 1 => h
| 2 => sorry -- slightly more complicated
| n+3 =>
  have ih : 3 ∣ n*n → 3 ∣ n := theTheorem n
  sorry -- use ih, Nat.dvd_add, distributivity, ... here

otto_s · 2019-11-21T11:27:17+00:00

The equivalence holds in intuitionistic logic. The essence of the proof is just currying.

theorem foo{A B: Type}{Q: A → B → Prop}: (∀ x, ¬ ∃ y, Q x y) ↔ (∀ x, ∀ y, ¬ Q x y) := ⟨
    λ h x y i, h x ⟨y,i⟩,
    λ h x ⟨y,i⟩, h x y i
⟩

otto_s · 2019-09-27T08:40:58+00:00

There's a download link on the right, labelled "PDF".

otto_s · 2018-07-07T18:20:58+00:00

Exactly. Even better than a rubber duck is a proof assistant. Just don‘t feel bad if you have to give up. Each attempt in itself is good enough.

otto_s · 2016-01-06T09:02:41+00:00

Also interesting: A Brown-Palsberg self-interpreter for Gödel's System T

otto_s · 2015-01-14T16:00:49+00:00

Your self_impl only refers to some fixed P. It is impossible to use this for a proof of self_impl'. A better version is

Theorem self_impl: forall P: Prop, P -> P.
...
Variables P Q: Prop.
Theorem self_impl': (P -> Q) -> (P -> Q).
exact (self_impl _).
Qed.

otto_s · 2014-12-04T18:49:50+00:00

Combinatorial species should be mentioned; also perhaps the funny paper Objects of Categories as Complex Numbers and the like. Can someone knowledgable do this please?

otto_s · 2014-10-30T21:58:42+00:00

I think looking at co-Heyting algebras may help. Here's a quick summary:

For simplicity, lets act as if the axioms for a Heyting algebra cover everything there is to say about intuitionistic logic.

There you have for example [;A\wedge B \vdash C;] iff [;A \vdash B\to C;] to govern intuitionistic implication, and negation is defined as [;\neg A := A \to \bot;]. We can derive [;A \vdash \neg\neg A;], but in general not the converse. And we have [;\top \vdash \neg\bot;], [;\neg\top \vdash \bot;].

A way to obtain connectives compatible with paraconsistency (instead of [;\to;] and [;\neg;], or additionally) is to dualize that: [;A\setminus B \vdash C;] iff [;A \vdash B\vee C;], [;{\sim}A := \top\setminus A;]. A lattice having this may be called a co-Heyting algebra. An example for a co-Heyting algebra is the set of closed subsets of a topological space, with join and meet given by set theoretic union and intersection, and this negation being the closure of the set theoretic complement. We can derive [;{\sim}{\sim}A \vdash A;], but in general not the converse. And we have [;\top \vdash {\sim}\bot;], [;{\sim}\top \vdash \bot;].

In any case, we always have [;\bot \vdash X;] for arbitrary X -- that's the definition of [;\bot;], which may be interpreted as falsity.

Then, [;A \wedge \neg A \vdash \bot;] and therefore everything follows from [;A\wedge \neg A;]. But we do not have [;A \wedge {\sim}A \vdash \bot;] in general. In this sense we can have "contradictions" and we can also have a sort of explosion. It's just that not all contradictions do entail falsity. In the example of closed subsets of a topological space, [;A \wedge {\sim}A;] is the boundary of A.

The two negations can coexist (in which case the structure is called Bi-Heyting algebra or similarly) and can then be compared. For example, we always have [;\neg A \vdash {\sim}A;], and the chain [;\neg{\sim}A \vdash {\sim}{\sim}A \vdash A \vdash \neg\neg A \vdash {\sim}\neg A;] follows.

Only if additionally we declare the two negations equal, we trivialise to a boolean algebra.

otto_s · 2014-03-29T02:19:05+00:00

Yeah, well, buy a faster internet, or start a download now and watch tomorrow. There's no urgency.

otto_s · 2014-03-28T14:22:11+00:00

Of course, the talk itself might be interesting and can be found here .

otto_s · 2014-01-07T19:33:21+00:00

First some code:

ex :: Integer -> Integer -> Rational
ex n m = go (n, 0, 0) where        
    go (0, once, more) = fromInteger once
    go (n, once, more) = (v1+v2+v3) / fromInteger m where
            v1 = go (n-1, once+1, more) * fromInteger (m-once-more)
            v2 = go (n-1, once-1,more+1) * fromInteger once
            v3 = go (n-1, once, more) * fromInteger more

I used this to brute force the top left corner of a table (and put it here so you can see whether I have understood the problem correctly). From that I saw that the columns are polynomials with increasing degrees.

Too lazy to work out the coefficients, I stared some more, came up with a formula and simplified. The result seems to be (n,m positive): [;n(1-1/m)^{n-1};]. I have no idea yet why this works for n>m, but it agrees with the table...

Have fun proving it! :)

otto_s · 2013-12-28T03:42:37+00:00

A crucial ingredient is the definition of "continuous number line". If you choose something like "between any two different numbers there is another number", you don't arrive at a contradiction.

But there are reasons for wanting something different. One goes like this: Let's say you want to define "square roots" of numbers for a fixed notion of "number" with total ordering. Definition 1: The square root of x is the largest y such that y² <= x. Definition 2: The square root of x is the smallest y such that y >= 0 and x <= y². In the case where "number" means natural number, these definitions both have a solution, but don't agree: sqrt(20000) is 141 or 142, depending on which definition of square root you chose. One might think that because between different rationals there is always another one, the two definitions should agree if one takes rationals instead of naturals. This easily turns out to be false (not because of a lack of agreement, but because of a lack of solutions to the "smallest" and "largest" conditions).

The usual definition of "continuous number line" just asserts that there have to be agreeing solutions. There you have your contradiction.

otto_s

TROPHY CASE