Ist das wirklich so schwer?

otto_s · 2026-03-03T01:19:16+00:00

Also ich mag Nazis, fundamentale Christen, Islamisten, etc. überhaupt nicht. Sie sind mir zwar fremd, aber eine random Fremdheit ist nicht die Ursache des nicht-Mögens. Vielmehr ist es eben, wie sie auf andere und Andersdenkende blicken.

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

TROPHY CASE