@user525966 Hmm. In case what I said wasn't clear, the Fitch-style system I gave you has all the basic boolean operations inbuilt, so there is no need to 'define' any of them.

In contrast, the Hilbert-style system in your question only has "¬" and "⇒" as inbuilt boolean operations, and then they 'define' other boolean operations in terms of those two, as explained in my post. I do not think that is the right way to go, since the concepts of "∧" and "∨" are actually derived from the natural language "and" and "or".

This is why if you look at the way the boolean operations are handled in the Fitch-style system, you should notice that it is totally transparent. For example, if you can deduce A and B in some context, then of course you can deduce "A∧B" in that same context, and vice versa.

I think that's actually the reason Fitch style proof systems are the ones taught in most American philosophy departments. They're the ones you use when you want to actually prove something without fiddling with a lot of moving parts.

@MaliceVidrine That's interesting. Now I wonder why the mathematics departments are not doing the same...

I don't think it's that they don't use Fitch systems in math departments, but I think there's more variation.

The philosophy department at my university teaches the Tableaux system, which is extremely annoying when it comes to quantifiers. You have to keep going through the existing nodes with active children in a certain manner in order to have the semantic-completeness property. And they didn't even teach that "certain manner" properly.

I like tableaux. Though from a pragmatic standpoint, they take up too much paper :P

My favorite approach in practice is still the "main method" from Quine's Methods of Logic. The spirit is the same as tableaux (start from some assumptions, try to hit a contradiction), but the presentation is decidedly Fitchian.

Of course, I'm far from impartial regarding Quine.

Hahahaha...

Anyway have you actually seen them teaching and using Fitch-style in the mathematics department? I think one of the major reasons a lot of mathematics students have a shaky logic foundation is because whatever logic they are taught in first year are not actually applied to the other courses.

Which is sad, really, because I noticed a lot of students having trouble with problems that basically solve themselves after expanding definitions and logical manipulation, and also making invalid quantifier switches when the quantifier depth goes up.

I have not seen Fitch in a math department, no, but at this point I've met more mathematicians in the UK than America. :P My own current university doesn't teach any specific proof systems in their "introduction to proofs" class, I don't think.

Which I think is dangerous, because having the formality to refer back to makes for good hygiene.

@MaliceVidrine Yea. I often say that once a student masters a Fitch-style deductive system, they no longer need it on paper most of the time (because they can do it mentally).

@MaliceVidrine Hmph... That book does not seem freely available online. Do you know of a slick presentation of the method somewhere?

Not really, but it's pretty lean. It's got only the truth functional rules, universal instantiation, and existential instantiation with the restriction that the variable needs to be new. So it doesn't use either of the quantifier generalization rules.

I see. Yea sounds like Fitch-style tableaux.

It's one of those things that definitely displays Quine's fondness for economy. It wasn't until later editions that he added a full Fitch style system, and he didn't seem to care for it much :P

Well I think standard Fitch-style is more 'natural'. When I want to prove a universal sentence, I want to deduce the inner sentence under the context of the bound variable.

Also, there is the thing that tableaux systems seem to depend on classical logic, whereas Fitch-style ones don't.

Yes, I think it was people telling him that that forced him to eventually add it :P

Aha. Haha..

And I agree.

Though I like how few variables I have to keep track of in his main method.

Though at this point, as I've said, I've started to become more fond of sequent systems, particularly for intuitionistic reasoning.

Is it really fewer asymptotically? I've never thought about that question. I did notice that standard Fitch-style has to include renaming variables to make things pragmatically convenient, but it felt like it didn't use any unnecessary variables.

And for that particular issue of variable renaming (to avoid shadowing) there's the de Bruijn indexing that entices me every now and then...

Which is that?

Where instead of a variable name you put an index that tells you how many scopes you have to go up to find the binding.

This can be used for both quantifier binding and λ abstraction.

As for whether it saves on variables a lot, I suppose it's not that the main method tracks fewer variables. It's that, at least in Quine's full system, there are variables that are tracked, and later dismissed, so that looking at previous lines for a "flagged" variable doesn't tell you off hand if that one is still off limits. You need to see if it's in one of his indented "hypothetical" environments.

So I think Main Method proofs can actually run longer, but it's quicker to check what your current variable restrictions are.

For example "forall x exist y ( Q(x,y) )" becomes "forall exists ( Q(v[2],v[1]) )" where v[k] is the k-th visible variable counting from inside to outside.

@MaliceVidrine Ah I see it sounds like my variant is not very different from that. I forgot that my variant is not like the usual systems. I don't have a rule that lets you go from "Q(x)" to "∀x ( Q(x) )", in part because of my desire to have every variable defined (bound). This also means that my variant works for the empty structure, unlike conventional first-order logic, though it is irrelevant in practice.

Aha. That seems similar in spirit to the syntactic version of Skolemization that Quine mentioned as an aside. In that notation, he just omitted the existential quantifiers and instead subscripted the variables that would be existentially quantified with the universally quantified variables they're within the scope of.

(I'm a slow typer)

I'm also a slow typer... about 70 wpm only haha..

So using that device, you could get rid of the existential instantiation rule entirely in his main method.

At the cost of secretly smuggling in a bunch of function symbols.

@MaliceVidrine Right. Have you seen the long list of Fitch-style variants here?

I have not! downloaded for future reference....

It's a bit too brief, and sort of assumes you already know what the possible variations are. But it's the only concise comparison I know of.

I really need to organize my documents....

Any time I get institutional access to journals, I download almost everything tangentially related to my interests.... But right now I just have a folder full of badly named PDFs :P

Hahaha..

It seems like in our age of the "tag" as an organizational device, there should be more file managers that have a tagging capability.

I put the stuff I download into a nice multi-level hierarchy of folders, just like statements in my proofs. =D

hehe

(It's been so long since I mucked about in PA that I'm having to get a renewed sense of how to work with encoding proofs. I just need to keep telling myself that it's good for me.)

Also, thinking about it, I think I scared off answerers to my bountied question by making it sound more complicated than it actually is. Do you mind if I throw a boiled down version at you?

@MaliceVidrine Haha.. I always forget Godel's β-function, because I think computability (rather than arithmetic) is at the core of incompleteness. Have you seen my post (pinned on the right) about the incompleteness theorems? I had a section on TC (theory of concatenation), which is even weaker than PA− and has no 'arithmetic' yet is essentially incomplete. It is much easier to understand encoding of sequences (and hence proofs) in TC.

Of course, to show that Th(N) is uncomputable (or that PA− interprets TC) one still needs the β-function...

@MaliceVidrine Sure, though I doubt I would be of much help because I know hardly anything about category theory.

It's not really, at its heart, a deeply category theoretic question, which I think is where I went wrong (it's just most of the people who deal with coherent theories are category theorists)

(And you might not have seen that linked proof of the incompleteness theorem before, if you haven't read Kleene's 1967 Mathematical Logic text, so it should be a fun read for you!)

The question is really just this: Am I right that "\vdash C or D" and "C and D \vdash False" entail "\vdash C or -C", intuitonistically?

(I still doubt myself on constructive proofs)

@MaliceVidrine Such questions can be phrased as follows: Can you prove it using my Fitch-style system minus DNE plus explosion?

And I have a copy of Kleene's Mathematical Logic somewhere, though I first encountered it when I probably wouldn't have appreciated it. I do, however, have his Introduction to Metamathematics right next to me.

@MaliceVidrine In my post the core undecidability problem (the zero guessing problem) is phrased in a similar style to the blog post that inspired my post. Kleene's text uses a purely mathematical definition, so the 'niceness' of the idea is 'obscured'.

Usually the more "mathematical" ideas actually make much more sense to me than the more computational treatments.

I'm one of those people to whom concrete examples and visualizations make things less clear, very often. :P

It depends, I guess. Of course the mathematical version is 100% precise, but if you know the halting problem, then the zero guessing problem is a nice tiny twist. There is a mathematical version of the halting problem, but in my opinion it is opaque because you have to set up programming (like Turing machines) inside mathematics, which is a pain.

You can tell me what you think of this particular 'niceness' after you've read it. =)

The zero guessing problem is pretty cute.

Aha so I caught you. =D

I was amazed when I first read it on Scott Aaronson's blog post.

I think I'm inexperienced enough with this stuff that I can't be amazed, but as with many things I am willing to believe that I don't fully appreciate it yet. (Hell, it was six years after learning basic category theory before I really appreciated the Yoneda lemma.)

@MaliceVidrine I guess it's mostly amazing from a theoretical CS viewpoint, because it abstracts out the core of incompleteness, instead of getting bogged down in technical but inessential details. This isn't to say it is easy to formalize 100% precisely (it isn't), but it means that almost anyone who understands programming and basic mathematics should be able to understand the entire proof of the incompleteness theorem.

Mathematically, this shows up in the fact that this proof relativizes trivially (as per my last section).

Aah, yes, it is nice from that viewpoint.

@MaliceVidrine So, about this question, since I can't prove it in my Fitch-style system for intuitionistic logic, the answer must be "no". =D

Hm. So where did I goof? Because it looks like D should be equivalent to -C...

Classically yes but not intuitionistically. In fact, you can prove the following intuitionistically:

> ( C or D ) and ( not not C and D implies false ) implies C or not C.

But not the one you want.

Now to prove that the answer is "no", without resorting to argument from my inability, one would have to construct a Kripke frame.

@AndrésE.Caicedo: Hello and welcome!

Hm. I'm trying to locate the particular step in my own proof where I infer something wrong.

Hello.

Hello!

@MaliceVidrine: But for the fun of it, here's how I thought about it. The last step in any purported proof of the desired conclusion must be explosion or ∨-intro or ¬-intro. None of them work.

@AndrésE.Caicedo: The question we are now discussing is this one:

I've somehow ended up with a "proof" this is the case, but it sounds like my proof went wrong somewhere. :/

So "D \vdash -C -> D" and "C\vdash -C -> D" should both be true things, and entail "C or D \vdash -C -> D" yes?

@MaliceVidrine Yea.

k...

So if "-C \vdash C or D", and "C or D, -C \vdash D", then this should mean "-C \vdash D", right?

Yes.

And from the second axiom above, we already have D \vdash -C.

@MaliceVidrine No.

How not?

Prove it.

=P

C and D \vdash False implies D \vdash C -> False. That's the implication rule. Like, the only implication rule.

Wait... Got to go for a while.

Oh yes you're right, so then your claim is correct.

I forgot that I can get "not C" from "C implies false".

So much for argument from inability.

Phew. I was questioning my reading comprehension more than usual :P

And if that's correct, then the situation is as much of a bummer as I thought :P

For completeness here is the Fitch-style proof:

If ( C or D ) and ( C and D implies false ):
	C or D.
	C and D implies false.
	If C:
		C or not C.
	If D:
		If C:
			C and D.
			false.
		not C.
		C or not C.
	C or not C.

nod

@MaliceVidrine And please post an answer to my question about Con(NFU) if you get it finished. =)

Will do what I can!

I'm trying to decide whether to try to interpret Con(NFU) directly, or interpret TSTU+Amb. Both have different tricky things to try and code.

Oh okay.

Thanks!

Again, this is not my wheelhouse. I just really want to take a stab at it because I should know how to do this sort of thing. Also I don't think I can talk Forster or Holmes into spending their time on it.

:P

@user21820 have you tried to prove that S : N -> N is injective in ZFC? where S is a successor function

that is, S(n) = n \cup {n}

@famesyasd It's true. Are you facing a problem proving it?

@user21820 yup. I thought that maybe you haven't touched it so I could suggest you a good exercise :)

@famesyasd Haha. I did it mentally many years ago, so I may have forgotten how to do it. =P

nvm I'm pretty sure it's correct, what's weirded me out was that if we use double induction in the reverse way the proof doesn't work but I think that's fine I remember same thing happening then proving associativity of multiplication on natural numbers not all the inductions work, And the second thing I have not used the hypothesis of the second induction, only the first one. But that also happens with some other induction proofs

@user21820 I guess I am just confused on the fundamentals here

before I even delve into the fitch thing

I'm still struggling to really / truly / honestly understand all the metalogic stuff

@user525966 metalogic is just another branch of mathematics like algebra or geometry or physics, why are you trying to understand specifically metalogic? Maybe you are actually interested in how math can be formalised and not about theorems about math itself? because that's what metalogic is about (I might be all wrong on this)

I am trying to better understand things like $\vdash, \vDash, \to$

how we separate things like premise and conclusion

how we define proving

what axioms and inference rules are actually doing

which things are defined and which things are consequences/things that follow as a result of defined things, etc

@famesyasd Let me get back to you later on this.

@user525966: That is why I suggested actually using the Fitch-style system. It is pointless to attempt to learn meta-logic unless you already understand how to use an actual deductive system for logic itself.

I mean I understand the "definitions" of some things as-stated on Wiki but in terms of what they actually do or how they're used, I get lost

I don't understand what the Fitch system is for / what it's doing

Did you look at the examples I linked you to or not?

I did

There are three posts linked from here:

I asked you to pinpoint the first line that you cannot understand in any of them.

That would help us both figure out what exactly you don't get.

First lines in all of it

It's already starting into stuff I don't understand yet without knowing what's underneath it

Okay the first line is simply specifying a context under a certain condition.

Since you are familiar with programming, you already know what an if(...){...} block means.

That "If C:" is doing exactly the same. The lines underneath it are claimed to be true only under the condition that C is true.

yes but we're already getting into stuff that's higher-level than what I am trying to grasp

No it is not. The stuff you keep asking about is higher level, but you don't know it because the text you are using is not pedagogically suitable for learning basic logic.

the moment we start talking about "this value is true" or "simplifying / proving an expression" etc it's already assuming we've accepted how the mechanics work, syntactic consequence, semantic consequence, defining the operators in all this context, inferring things, etc

No that is not what I mean. The goal is indeed that we want to only deduce true sentences, but this "true" here is the intuitive notion and not the formal definition. I had the impression that you already understood basic logic, when we had our previous discussions. It seems you don't, so we'll have to start from scratch. Forget everything we discussed before.

I'll only assume you understand programming. You know C/C++/Java?

I already do know how to do things within the system of logic but I am trying to pretend I know absolutely nothing and start from scratch, as if I were an alien from another planet who is unfamiliar with everything

and yes C/C++/Java/Python

Okay good.

We start with propositional logic, using C.

I wish to write a program of a certain form that has no assertion error.

You know what is assert right?

yes

We can also use false, for convenience.

For example (inside the main method after the appropriate input statements):

if(P)
{
  assert P;
  assert Q;
}

This is a possible program I can write, but it has an assertion error on some inputs. You know why, right?

For our convenience, we shall call this kind of restricted programs propositional programs or PPs for short. And we say that a PP is valid if it has no assertion error on every combination of inputs.

Our goal will be to write only valid PPs.

The above PP is invalid.

Is the following PP valid?

if(P&&Q)
{
  assert P;
  assert Q;
}

@user525966: Can I go on? Can you respond?

Sorry thought it was a trick question due to lack of parens

But otherwise yeah, possible for Q to be false

Right, for the first one that is one way to make it have assertion error.

Is the second PP valid?

as far as I can tell yes

I want you to be 100% sure.

Consider how the program runs; if it enters that if(P&&Q) body at all, it must be that (P&&Q) evaluates to true, so...

if I am to be 100% sure then no it would not run without the parens :P

Hmm what "parens"? I thought I am writing 100% correct C code?

assert(P) vs assert P

I'm sure the latter is permitted in C/C++/Java. I've used it before.

In fact, that's the 'default' syntax.

I don't have a C compiler at hand, and the online ones don't even support assert, so never mind. Just assume I'm correct hahaha..

Java definitely permits no brackets.

Anyway, let me repeat our goal:

We wish to achieve this goal because it means that every assert statement in the PP is asserting a true boolean expression regardless of the inputs.

yes

In particular, if the last statement of the PP is outside any if-structs, then it asserts a truth regardless of the inputs.

To achieve our goal, we shall devise a small number of rules to govern the kind of PP that we will write.

And we want to do so in such a way that it is obvious why those rules will ensure that we can only write a valid PP.

I hope it is obvious why we want valid PPs, because that corresponds to the intuitive goal of asserting only true statements in any context, where here the context of a statement is simply all the if-conditions guarding it.

@user525966: So far so good?

i suppose

That aspect still eats at me a little

Which aspect?

It seems conceivable that from truth we would want to deduce both true and false things if we so chose

rather than strictly true

trying to understand why we'd want to stick with just-truth-alone

Hmm that's philosophy, but clearly we can't make predictions if we cannot tell which of the deduced statements are true and which are false.

If however we ensure that we can only deduce true statements, then we can safely make predictions based on our deductions.

why wouldn't we be able to tell apart which are true and false?

At this level you may not understand, but it's basically impossible to do so without a deductive system.

And so right now my aim is just to make sure you fully understand a deductive system.

I mean we do have the concept of truth-preserving as well as false-preserving, I believe

and likely those that cross over in either direction

And note that I am careful with that issue here too. There are general programs, then there are PPs which are not valid, and there are PPs which are valid. Sure you can write any program you like in your free time. But right now I only care about valid PPs. Furthermore, it is in fact impossible to tell whether an arbitrary PP is valid or not! That is why I said we shall impose some rules to further restrict to a small collection of PPs that we can ensure are valid!

(I gtg, but I'm on mobile so will still be here, just responding slowly with phone)

@user525966 I actually have to go really soon too.

ahh ok

will talk later then :) thanks again

Sure! You're welcome!

@user525966: I better fix my above claim; PPs correspond to propositional logic, and so it is possible to tell whether an arbitrary PP is valid or not. However, later for first-order logic it will become impossible. So it is important to go to a rules-based system.

Okay see you later!

@user21820 I figured out that the second induction was not needed

@famesyasd I was kind of thinking that your claim here might be needed to prove the injectivity... However, it should not be that you're not using some part. Which you just beat me to it while I was typing my comment.

I need to type faster.

however, since x != y (we are using this statement several times, now and in previous part) we have exists t (t in x and t not in y or t in y and t not in x)

in both cases it follows that either t = x or t= y and thus either x not in x or y not in y contradiciting x in x adn y in y

@famesyasd Once you get x subset y and y subset x you have x=y by extensionality.

oh right!!!

This is what happens when you do too much ZFC.

=P

Like coding in assembly.

I'm about to do recursion

finally

Lol but seriously this is not the way to learn basic mathematics.

:((((

It is part of the way to learn ZFC.

But if you are actually interested to have 100% formalized basic mathematics, you shouldn't be using ZFC.

All the encoding into ZFC objects is just distracting from the mathematical content.

@user21820 what would you recommend?

coz I don't understand, isn't ZFC heavily used in mathematics?

and what do you mean by basic mathematics

@famesyasd ZFC is a viable foundation for most of modern mathematics, in the sense that there is a way to encode most of modern mathematics into ZFC. It does not mean that ZFC is the most natural foundational system that can support this goal of formalization.

By basic mathematics I meant elementary number theory, which is what you can prove using PA. To deal with basic analysis, you could use higher-order arithmetic.

Except when studying ZFC, I find it rather pointless to prove properties about N that are peculiar to ZFC, such as the one you mentioned. Yes, it is an important thing to know about ZFC, but it is peculiar to ZFC and completely irrelevant to ordinary mathematics.

Ordinary mathematics should, in my opinion, be formalized in a foundation that already has at least this axiomatization inbuilt.

So it boils down to whether you want to study ZFC in particular or whether you want to formalize ordinary mathematics.

@user21820 how do you define integers in PA^-?

and other things without sets I don't get it

So you may be familiar with the integers as a quotient of naturals over some equivalence relation. That of course doesn't work in PA because PA doesn't have 'sets'. That is why it is most convenient to move upward to higher-order arithmetic to do analysis.

okay so what is higher-order arithmetic

and also the other thing I don't get is how come if you can prove some theorem in ZFC via an axiom of choice for example, would you be able to prove the same theorem here?

@famesyasd In higher-order arithmetic, you have a couple of sorts (which I often call types). In my variant, there are 0th-order types N and bool, interpreted as "naturals" and "booleans". Given any k-th order types S and T, you have a (k+1)-th order type func(S,T) which is interpreted as the collection of all functions from S to T. Any k-th order type is also an m-th order type for every m > k.

The linked axiomatization of PA uses only quantification over N, so it 'sits within' first-order arithmetic.

In higher-order arithmetic, you can quantify over any type, including func(nat,nat) and func(func(nat,bool),bool) and so on.

This allows you to build lots of things. Subsets of a type S can be almost directly represented as members of func(S,bool).

In higher-order arithmetic, given any types S,T you are allowed to build a function f := ( S x ↦ E ) where E is a term that has type T in the context where x has type S, and this f as you'd expect denotes a function from S to T.

Maybe an example is good here. Let's prove Cantor's theorem that there is no surjection from nat onto func(nat,bool)!

how do you define surjection

Here is the theorem:

> not exists F in func(nat,func(nat,bool)) forall g in func(nat,bool) exists n in nat forall k in nat ( F(n)(k)=g(k) ).

okay

So you can easily prove it, in Fitch-style or whatever.

Oops I should have used "⇔" instead of "=", because I used "bool".

The same proof works for func(nat,nat) where the theorem would use "=".

This will give you a feel of how higher-order arithmetic works. Basically, you know the type of every object you're dealing with, and it is something built from nat and bool.

@user21820 what to do with a proof in zfc that uses axiom of choice? do you use some of AC interpretation here or what?

@famesyasd Higher-order arithmetic in itself does not have choice. But you may be surprised that almost no ordinary mathematical theorem that can be stated in higher-order arithmetic needs choice. We could add it in if desired.

As for equivalence relations, a binary relation on nat can be represented by a member of func(nat,func(nat,bool)), via currying. But if you want to have convenience you could just as well throw in Cartesian products of types, namely given any types S,T there is the type S·T, and also throw in projection functions such that if x in S·T then x[0] in S and x[1] in T.

(Above I used "·" for product... because using "*" makes some unwanted italics...)

@famesyasd You may have heard of the theorem that if ZFC proves an arithmetical sentence than ZF already does. That is called arithmetical absoluteness. However, I am not sure what you need in order to prove arithmetical absoluteness... I know that ZF suffices though.

This does not contradict what I just implied by saying we can add in choice if desired, because indeed ZFC can prove some higher-order arithmetical sentence that cannot be proven in higher-order arithmetic without choice.

For example, that the reals have a well-ordering.

To give you an idea of how we can state such things, given f in func(nat·nat,bool) we can say "f is a total ordering" by saying "forall x ( f(x,x) ) and forall x,y ( f(x,y) implies f(y,x) ) and forall x,y,z ( f(x,y) and f(y,z) implies f(x,z) ) )".

And to say "f is a well-ordering" we can say "not exists g in func(nat,nat) forall n in nat ( f(g(n+1),g(n)) )".

I have just shown how we can talk about well-orderings on nat. You can similar express the notion of well-orderings on func(nat,bool). But "exists well-ordering of func(nat,bool)" cannot be proven in higher-order arithmetic without choice.

oh I see

But in most ordinary mathematics you don't need such a well-ordering...

And anyway I think you can see how we can construct integers and rationals and reals in higher-order arithmetic.

So almost all real analysis can be done quite naturally.

@famesyasd: Anyway I need to go.

See you!

yeah I see how they can be constructed but I need to reread all of this, anyway I decided to beat last topics in ZFC and I just need a couple of days to cover them, later I will look into HOA, also AC doesn't really makes sense, do you agree? It essentially states that we can always describe an infinite set despite of how complicated it can be

@famesyasd Hmm.. I think it strongly depends on the foundational system as a whole. If it has a countable intended model, then AC does make sense because you can always pick the smallest witness. However, ZFC was invented with an intended interpretation of P(N) as uncountable. So there is no longer a good justification for AC.

And sure if you want to learn ZFC then you need to learn all the stuff related to encoding in ZFC. =)

@user21820 tldr?

@LeakyNun If want to know exactly how to formalize mathematics in ZFC, then you need to learn how to obtain basic objects like a model of PA in ZFC. If you just want to do basic mathematics formally, PA or higher-order arithmetic will suffice.

PA is just an inductive type :P

Anyway, I better go now. You two can carry on. =)

@user21820 No, I'm going to sleep

see you all tomorrow