@famesyasd From R0(0,x) you get 0=0 implies x=c by definition of R0. Same for y=c.

@famesyasd It's just me defining what is a relation from nat to A. Just read rel(nat,A) as the type of all boolean functions on pairs whose first item is in nat and whose second item is in A. This is the essence of what a relation is (which in ZFC would instead have to be encoded as a subset of nat times A).

@famesyasd I omitted it because it's quite short and I was lazy. By definition to prove G(R0) you just need to prove R0(0,c) and forall k in nat ( forall x in A ( R0(k,x) implies R0(k+1,F(x)) ) ). I think you can definitely do that.

Let me know if you hit any further obstacle.

@user525966 I agree with LeakyNun that before you attempt to study logic as a mathematical object you need to know how to use logic itself. If you wish to continue from where we left off, then we can get to an actually usable system. I don't know whether I said before, but it is impossible to understand logic if you don't know how to use it. And knowing how to use it only requires you to know how to follow (writing) rules strictly, so it is definitely what everyone can learn if they wish to.

@user21820 why, you also need to prove that forall k in Nat, x in A (R(k,x) implies R(k+1,F(x))

@famesyasd I wrote exactly that, with R0 in place of R. You want to prove G(R0), after all.

Informally, R0 is just the relation that maps 0 to c and every other natural to every element of A.

So it is easy to check that it is 'closed under the recursion'.

@user21820 okay then and how do you conclude that (0,x), (0,y) in R0 lol

you'd need to prove that if 0 = 0 then x = c lol!

@famesyasd From S(0,x) and G(R0) you get R0(0,x).

You can't do it without using the given assumption of S(0,x).

I don't understand how did you prove G(R0) then and what it is, I can see that you can show that (0,c) in R0 easily but not for other things lol

@famesyasd So you are unable to fill in the first "..."?

@user21820 can you write out what R0 is in pure FOL so that I can understand its definition

also sorry, I got to go I'll come back in 3 hours

I don't think you don't understand its definition. R0 is just a simple relation, which in ZFC would be encoded as { [k,z] : k in nat and z in A and ( k=0 implies z=c ) }. I think you're missing that "forall k in nat ( forall x in A ( R0(k,x) implies R0(k+1,F(x)) ) )" is vacuously true.

Here is the proof of that first "...":

	R0(0,c).
	Given k in nat and x in A such that R0(k,x):
		If k+1=0:
			Contradiction.
			F(x)=c.
		R0(k+1,F(x)).

So from this you can conclude that G(R0); namely R0 satisfies the recursion.

Anyway, see you later!

@user21820 I can use it fine, it's the rules / definitions that are hard

@user525966 Please show me. Prove this theorem within PA using Fitch-style.

I don't understand the whole pushing-fitch-style thing and I'm not jumping to first order logic yet

I'm still trying to get a handle on prop logic systems

@user525966 Sorry but if you want to learn to use logic you are going to have to understand a usable system. Hilbert systems are unusable.

Why do you say that

Not a single mathematician in the entire world will ever use a Hilbert-style system in their actual mathematical work, for obvious reasons.

Not obvious to me why that would be the case

Because all you have seen so far are trivial toy examples.

It can still do the same stuff as other systems does it not, just built with different axioms and rules

@user525966 "It can" is not the same as "you can" or "you understand completely how it works". I don't want to argue with you. If you want me to teach you I think you should at least invest effort into something that I know will pay off.

I'm just trying to learn -- I'm not arguing either but if you are going to interpret questions that way, I'm not interested in continuing this conversation

@user525966 If you want to learn, then please learn the system I tell you to learn.

If you want me to agree that one system pays off over another I'd rather learn/Intuit/see why it's indeed the case rather than take something on faith and never end up learning the difference firsthand

@user525966 I never asked you to agree on that yet. I said clearly before that only after you have learnt a Fitch-style system then you will fully understand all the other systems as well.

If Hilbert systems suck then I'd rather see why they actually suck

You will. After you learn a Fitch-style system.

What is the merit of a Fitch style system and what does it do / what does it cover / what is the alternative?

Sure I'd agree with that, but once those operators have been defines what stops us from using the convenient versions instead?

I'd imagine Hilbert made this system for a reason, he's one of the greatest mathematicians of all time is he not -- what was his intent?

@user525966 Defining enough of the basic boolean operations does solve one problem, but only one.

@user525966 No! He did not make his system for practical use!

I don't expect that he did, no

But what was his reasoning for it?

He made that system clearly so that he can analyze logic from the outside.

Only one problem? How so?

Most of the practical problems will show up only when you get to first-order logic, but I will give you an example in propositional logic.

Prove the following:

(2) ( A or B ) and ( B or C ) and ( C or A ) implies ( A and B ) or ( B and C ) or ( C and A ).

(The conventional precedence from highest to lowest is: not, and, or, implies.)

@user525966: See if you can do them easily, and post your proofs here.

@user21820 What I mean is, let's say we define $\land$ and $\lor$ in terms of $\to$ and $\lnot$, prove distributive laws and such, and then for that first one do something like:

which is like proving $P \to P$ is true

@user525966 Yes I assume you have already defined those. But what you just wrote is not a proof.

You are not even using a Hilbert-style system.

You are just doing boolean algebra.

To what extent? I'm just showing that the lefthand side and righthand side boil down to the same thing

which shows the implication is true

No.

You claim to be able to use a Hilbert-style system. In such a system, the only inference rule is modus ponens.

You cannot do any kind of algebraic manipulation.

If you insist on doing anything else, you are merely proving my point that a Hilbert-style system has no practical use.

I'm not claiming any such thing, I'm asking questions

I assumed by that you were asking me to show you why.

Yeah that's not the same as me "claiming to be able to use a Hilbert-style system"

I have just done so.

@user525966 Fine. I had interpreted you to be claiming so because you kept disputing my claim that Hilbert-style systems have no practical use.

Again I'm not disputing! I'm asking why

I know. It's not that I don't want you to be critical or skeptical. But sometimes it seems to be an inefficient use of our time if you object to too much of what I tell you.

Just because I can't personally do something yet does not convince me that it's not worth learning for example

I'd prefer to see why it sucks / why it's a waste of time, or at least see how I'd do it if I needed to even if just on principle, etc.

As I imagine you would be able to do

Yes I understand that.

And my answer to that particular question above is that once you actually force yourself to use only modus ponens as your inference rule, all your proofs will become ridiculously bloated.

Would this be another example of what you mean: proofwiki.org/wiki/Law_of_Identity/Formulation_2/Proof_3

Yes. In a Fitch-style system it would simply be:

If P:
  P.
P implies P.

There is a reason I did not use that as an example though, because people can easily say they can add extra axioms like ( P implies P ) to avoid that long-winded proof. But that does not solve the more general problem of bloat that affects every proof and not just that one.

Do most people use ND for prop logic?

Hence I gave two sufficiently complicated tautologies that one cannot argue should be just axioms.

@user525966 Most mathematicians use 'common sense', and so not a few have made serious logical errors in their mathematical work. Those who know logic properly tend to think in Fitch-style even if they never write it that way.

Natural deduction comprises three main traditions:

(1) Tree-style.

(2) Sequent-style (like LK).

(3) Fitch-style (like mine).

For purely propositional logic, simple tautologies can be verified via truth tables and people may not bother to use a deductive system.

Does Fitch-style still work with Hilbert systems?

Or is it only a ND concept?

@user525966 Well the whole point of a Hilbert-system is to have only one inference rule modus ponens, so it is simply incompatible with the Fitch-style. You can easily see the disparities if you think about implementing a program to check proofs in either style. It is trivial to write a program for a Hilbert-style system for propositional logic, but not so easy for a Fitch-style system.

@user525966 I don't think of those as ND concepts. ND just stands for various styles that are 'natural' enough to be reasonably called 'natural'.

For that reason, logicians have never called Hilbert-style systems natural.

Got to go. Back later.

For example how would you prove the one you posted earlier, (A implies B or C ) implies ( A implies B ) or ( A implies C ), using Hilbert style?

Ok

@user525966 I won't, sorry. I can prove that I can do it, but it is a waste of my time and energy to actually do it. Here is how a Fitch-style proof will look like (the blanks are for you to fill in):

If A implies B or C:
	B or not B.
	If B:
		...
		A implies B.
		( A implies B ) or ( A implies C ).
	If not B:
		If A:
			B or C.
			...
			C.
		A implies C.
		( A implies B ) or ( A implies C ).
	( A implies B ) or ( A implies C ).
( A implies B or C ) implies ( A implies B ) or ( A implies C ).

The first assertion "B or not B" is not covered by the rules given in this post, but is an instance of LEM (law of excluded middle), which is usually better to have. Any instance of LEM can be proven from the other rules, so Fitch-style systems often leave it out.

@user21820 okay I see lol, nice. So tldr the main point is that uniqueness is indeed independent from existence and one can always show that with a little bit of rewritement? Like you did in my proof.

and thus the proof that I had is okay

@famesyasd Well I may probably have to retract my claim that you can mechanically rewrite the proof, because it may depend a little on how exactly you did it. But the notion that there should not be any new idea or technique required to 'separately' prove uniqueness should be correct.

The reason I say "depend a little" is because if you also used induction, but for some reason did it substantially differently, then you may end up with a tangle between uniqueness and existence.

If you individually prove uniqueness of mapping of each natural, then surely you can easily rewrite to prove uniqueness separately. But if the proof of uniqueness is an inductive one, as mine is, then it's not so clear.

In particular, I felt this when I realized that the uniqueness issue is inbuilt into the other construction of the recursive function via approximations, because all the approximations are already functions, and once you prove they are compatible then of course their union is also a function.

It is not inbuilt into this construction via intersection of relations closed under the recursion.

I assume you know the other construction, right?

@famesyasd Uniqueness as a concept is independent from existence. Recall the linear algebraic examples we did the other day. Frequently one will have a system of equations (say if you have more variables than there are equations) that will have infinitely many solutions. So a solution exists--but is not unique. Then with the equations defining the MP pseudoinverse we were able to show uniqueness without showing existence. That is, we showed that IF a solution existed, it would be unique

We were able to conclude this without even knowing whether or not a solution existed.

To say that one can ALWAYS have a separate argument establishing existence and uniqueness, at least in practice, is hard to say

@user21820 nope, don't know the other one.

@Secret Given your recent obsession with number theory I thought you might like Niven's Proof that pi is irrational : en.wikipedia.org/wiki/…