Are proofs by induction possible?

[umnikos]

I've been trying to create a custom induction block that looks something like this:

∀f.f(Z)→((∀x.f(x)→f(s(x)))→(∀x.f(x)))

The problem is that, as far as I know, f is not actually a function, so I can't use this block on anything like g(t(x),p(x)) by lambda abstracting it to f.

Is there actually a way to do induction somehow or is this a feature that needs to be implemented?

[nomeata]

When you say custom induction blook, do you mean within the UI? Or by editing the logics definitions in https://github.com/nomeata/incredible/tree/master/logics?

[umnikos]

From the UI by adding an extra proposition to a level. I don't know how the logics folder differs from that

[nomeata]

It allows you to define blocks, including interestingly shaped blocks, like this for the block for the ∃ quantifier:

- id: exE
  desc:
    elim: ∃
  free: ["P","Q"]
  local: ["c"]
  ports:
    in1:
      type: assumption
      proposition: ∃x.P(x)
    in2:
      type: assumption
      proposition: Q
      scoped: ["c"]
    hyp:
      type: local hypothesis
      proposition: P(c)
      consumedBy: in2
    out:
      type: conclusion
      proposition: Q

Maybe it would work, but to be honest, I can’t wrap my head arount it on the spot :-)

[nomeata]

Although, if I take the formula you gave, it seems to work quite nicely:

I used an annotation block to instantiate f with Q, but I could feasibly use any formula there. The missing inputs then look like what one would have to prove for induction.

I couldn’t think of a useful predicate to try it out with, especially not without equality in the logic.

[umnikos]

I couldn’t think of a useful predicate to try it out with, especially not without equality in the logic.

I already managed to define equality and addition in the following ways:

!a.E(a,a)
!a.!b.E(a,b)->E(b,a)
!a.!b.!c.E(a,b)->E(b,c)->E(a,c)
!x.!y.E(P(S(x),y),P(x,S(y)))
!x.E(P(Z,x),x)
────────────
E(P(S(S(Z)),S(S(Z))),S(S(S(S(Z)))))

(E being equality, P being plus and S and Z being peano numbers. The final proof is that 2+2=4) Except that when trying to prove !x.!y.E(P(x,y),P(y,x)) I ran into the problem that my definition of induction is not general enough to nest inside the Es and Ps...

[nomeata]

And you are sure that maybe with a carefully placed annotation block you can help The Incredible Proof Machine to figure out the right annotation? It otherwise has to guess, and may guess wrong.

[umnikos]

Okay somehow on my fifth try I managed to randomly change something to make it work and I don't know what that thing is :sweat_smile: Sorry for the issue, here's a picture of it for anyone looking at this in the future:

[nomeata]

Pretty cool, I just admit!

[nomeata]

BTW, out of curiosity: How did you stumble upon the kinda old project?

[umnikos]

BTW, out of curiosity: How did you stumble upon the kinda old project?

The site was mentioned by someone in the esolangs discord server and when I checked it out I found a better, hands-on explanation of what a proof checker actually is and what math is fundamentally made out of than any introductory lecture on Coq :smiley:

Also, now would be a good time for me to learn a real proof checker because these proofs are getting ridiculously huge and I'm not even proving complicated things...

[nomeata]

Thanks!

Also, now would be a good time for me to learn a real proof checker because these proofs are getting ridiculously huge and I'm not even proving complicated things...

Heh, I agree :-D