@user525966 Sure, you can stick to propositional logic first. The Fitch-style system in my post applies to propositional logic as well; just stop before "Quantifiers". Two exercises you can try are to prove "A or not A" and "A or ( A implies B )".
@user525966 I'm not sure whether you saw the second sentence in my last comment:
The rules given there are the only rules you are permitted to use. So any other reasoning (including truth-tables) is not allowed.
@user525966 What you're doing here is something like boolean algebra, but that again is not the point of a deductive system. Like I said before, you will only be able to appreciate deductive systems when you move to first-order logic, but since you want to stick to propostional logic you at least have to learn a deductive system for propositional logic, such as the one I specified in my post. If you don't, you will not have a proper grasp of even propositional logic.
@MaliceVidrine This is not the right answer to the question.
@user525966 What you're asking is why you can write anything on the paper in the first place. And yes you're correct that you need either axioms or inference rules that permit you to do so. Otherwise, you can't write anything on the paper at all. Even though there are wffs, it does not imply that you can write them down.
@MaliceVidrine I agree the question is ambiguous, but I think for you to be consistent with your use of "can write" in the preceding comments, you should not say that you can write (P⇒Q) because it's a wff.
Anyway it's not that you don't know what I'm saying, but I think it's confusing for @user525966. =)
@user525966 No Hilbert-style systems are essentially the only deductive systems that use a single modus ponens inference rule. The Fitch-style system I linked you to has no axioms but has only inference rules. I don't want to say much about the difference between systems until you can actually confidently use one system. My suggestion is to learn the system I gave you, because I've successfully used it to teach a number of others in this very room before.
@MaliceVidrine I have taught quite a bit, but I still prefer face-to-face. It's quite hard to teach certain things without being able to wave my hands and point my fingers and make the right shapes in the air to get the point across. =)
I think it will be quite some time before I gain even that sort of experience. I kind of traumatized myself by giving a really bad talk at Cambridge. Since then I've resigned myself to being mostly a pedagogical hermit. :P
@MaliceVidrine Talks are quite different from teaching. If you mess up one class, you still have time to improve and make up for it in later classes. I did that a few times when I taught. If you mess up a talk, well, there's no follow-up talk haha..
@user525966 Yes, so sadly you're going to have to imagine me waving my hands and drawing imaginary diagrams in the air.
@user525966: If you want to see some examples, look under "Natural deduction" on my profile.
But yeah referring to the earlier question about writing-on-paper, I imagine PROP (as it's referred to in a few texts) is the collection of wffs, the set of everything we can write in terms of what's "allowed" or "interpretable" as a formula -- and anything else is considered gibberish we can't work with
and I imagine the stuff we can "write down" is the stuff we "know" but I don't know what this really means
I figure the stuff we "know" is the stuff we can claim to be able to attribute true/false to semantically, and everything else is just unknown and not considered in the two-valued system
The collection of wffs are basically strings that we can interpret to have a truth-value given the truth-values of every atom. I think that much you have understood from our prior discussion. Now a deductive system is about enforcing certain rules about what we can write down on an initially blank paper, so that every wff that we write down is true no matter what truth-values are assigned to the atoms. Does this make sense?
Of course, if you are not working within a deductive system, you can (by your free will) write down whatever you like, including "fiiecjurfusrlj" on paper.
Well, I suppose you aren't aware what is so good about PA. I know I'm talking about first-order logic again, but it's the most concrete example of usefulness. PA can prove a sentence that would be interpreted to state Fermat's little theorem. That in turn can be used to prove that HTTPS works (which explains why you can read this website). If we did not have a deductive system that allows us to deduce only true facts from true assumptions (the axioms), what we deduce would be useless.
In other words, a truth-preserving deductive system for first-order logic, plus the axioms of PA, allow us to make incredibly precise true assertions about natural numbers in the real world, leading to real-world benefits.
That is what is so important about truth-preservation.
@user525966 Yes! The Fitch-style system I gave for propositional logic, and the Hilbert-style system you have in your text, are both semantically-complete for propositional logic; every propositional tautology can be proven in either system, and more generally, if you have some axioms, then every wff that is true in every model of the axioms can be proven.
The full Fitch-style system I gave for first-order logic is semantically-complete for first-order logic; every first-order tautology can be proven in it, and more generally, if you have some axioms, such as the PA axioms, then every arithmetical sentence that is true in every model of PA can be proven.
Here is another way to view this last point. Our real world W empirically behaves as if natural numbers encoded in a computer, with the standard arithmetic operations, form a model of PA. So PA is appears to be a true description (the axioms are true) of a part N of W. We would like to be able to deduce every truth that must surely hold for that part N of W.
If there is a sentence Q such that PA can neither prove Q nor prove (¬Q), then by semantic-completeness we can conclude that PA is actually an incomplete description of N, since there must be two models of PA that disagree about the truth-value of Q. In particular, there must be a model that disagrees with W about whether Q is true or not!
We can of course patch up this incompleteness by adding either Q or (¬Q) as an extra axiom on top of PA, according to whether we believe Q to be true or false for N (the naturals encoded in our computer, say in Python).
Another side of that is that completeness means that your notion of semantics doesn't have side effects we don't want. Imagine if we came up with a new semantics for the natural numbers such that every "model" of PA proved -Con(PA); given what we know about our usual semantics, we'd realize we had made up a bad semantics that was forcing things to be true that can't be proven in our logic. Completeness is the property that assures us that our usual semantics aren't doing this.
@user525966: Interestingly enough (though it's okay if you don't get what I mean), PA turns out to be indeed incomplete in this sense, and worse still we will never be able to 'completely patch up PA' so that every truth about N can be proven. That was essentially Hilbert's goal (to find a complete foundation for all arithmetic), and it is dashed completely by a suitable generalization of Godel's incompleteness theorem.
@MaliceVidrine This is definitely beyond @user525966 right now, but I'm curious what exactly you mean by your remark. Can you give a more precise statement?
@user21820 - I'm trying to get at the negation of completeness: a hypothetical situation where something is true in every model but not provable from the theory. it's difficult to get at well, though, because it's so unnatural :P
Obviously it wouldn't be the usual version of "model"
Yes, I was trying to get at it without delving into intuitionistic logic, which is where I'm most familiar with completeness (with respect to certain categories) failing.
Well for the example of PA, you would be able to find a sentence with one unbounded quantifier that is true in all (classical) models but cannot be proven or disproven without double-negation elimination. I think one doesn't need LEM for bounded quantifiers, due to induction. Is that right?
And I had a prior conversation in here where I argued that, once you accept LEM for Σ1-sentences, the same philosophical argument ought to make you also accept LEM for all arithmetical sentences, by meta-induction on the quantifier depth. =)
I think there is a certain school (was it Russian?) that rejected full LEM but accepted a limited form, which was essentially LEM for just Σ1-sentences...
@MaliceVidrine: What do you think? Just curious... =)
I can't comment, really, mostly because of woeful ignorance regarding Robinson Arithmetic. In general, I'm also not sure how to answer "shouldn't one accept LEM" style questions since I see classical logic and intuitionistic logic as being about different things :P
@user525966: Have you had a look at the examples of Fitch-style proofs in propositional logic linked from my profile? Please ask here if you have a problem with any specific step. It may help you understand the rules far better than just my English explanations.
@MaliceVidrine Wow. What was your motivation for returning to academia?
I discovered I loved mathematics unfortunately only after graduating with a psych degree, and it was a long time before I could afford to take another stab at it.
After being good enough at my hobby to get an invitation to kick it at Cambridge a bit, and not getting scared off, I decided to make a proper go of it.
Though initially I was at Cambridge to work with Thomas Forster's PhD student Adam Lewicki on the category theory of New Foundations. The last couple of years I've kind of taken a diversion.
It turns out, whether you study the classical model theory of NF or its category theoretic properties, it's still a frustratingly opaque theory. :P
Ooh, that's a really interesting question. Not one I can answer off hand, but my gut feeling is yes... Bare NFU is really weak. I'll give this some serious thought.
NFU is also pretty fascinating even if its consistency questions are simpler. Mostly because natural extensions make it so strong so fast. If you add Infinity + Choice + Small Ordinals (the assertion that for every property there's a set such that its strongly cantorian ordinal members are exactly those that satisfy the property) gets you close to ZFC+Measurable cardinal in consistency strength (I forget the exact strength).
@MaliceVidrine I thought that is just because "cantorian" stuff are essentially importing ZFC into NFU (via the back door)?
I was sad that NF[U] couldn't make sense of Russell's collection { x : x∉x } though. I view it like a categorization that does not terminate when used on itself, which seems conceptually well-defined to me.
Essentially. The "small ordinals" are the ones for which work for the usual proofs of transfinite recursion, and such that every such ordinal is the order type of the ordinals below it. So most natural axioms strengthen the properties of this class of ordinals.
er, I wrote two sentences into each other.
Read: "The small ordinals are the ones" instead of how that sentence actually began.
There's a version of NF with proper classes, ML, and one of the informal goofs that Quine made in it was he assumed the natural version of the natural numbers would be a set. But it's actually impossible to prove, and assuming that it's a set gives you full induction over the natural numbers, which is actually quite strong. Forster thinks the assumption that it's a set might actually make it inconsistent, but neither of us managed to prove it one way or the other at the time.
I have never understood why set theorists think that impredicativity makes sense in set theory. A lot of axioms have the general form "if certain conditions hold then certain collections are sets" and "set" in classical set theories means essentially an indicator function on the entire universe. But the comprehension axioms allow one to quantify over the whole universe... In MK one says that a subclass of a set is a set, but that is worse. (An RE subset of a recursive set may not be recursive.)
Impredicativity definitely seems like a bludgeoning solution to the problem it was designed to solve. I realize it took some time to understand that fully, historically, but at this point I find it odd that anyone would be philosophically predicativist.
But there is actually a rather compelling case that one does not need all that impredicativity for ordinary mathematics. ZFC where both Specification and Replacement are restricted to bounded quantifiers is still strong enough to prove practically every mathematical theorem that didn't arise in set theory or modern logic.
True. As a topos enthusiast I certainly can't argue against Mac Lane set theory on that front. In fact classical Mac Lane is really even stronger than you need.
I just had to take a differential equations course, and rarely encountered a non-constructive proof.
I don't have a personal problem with impredicativity except for the doubt of soundness, hence my words "somewhat predicativist". In particular, as of now I don't think full second-order arithmetic is unsound, even though some logicians here do!
@MaliceVidrine In fact, full higher-order arithmetic (over many-sorted logic) suffices for most practical applications. But if we like to have a sufficient grasp of order theory, say the well-ordering theorem, then yea we need to go to a set/type theory, but even then ZC with bounded Specification is more than enough.
This is actually something I'm not a hundred percent clear on, and this may be a silly thing to wonder: we have soundness and completeness theorems for the Mitchell-Benabou style of higher order logic with respect to topos semantics. it seems like this would entail very nice things for the second order fragment, but I can't quite persuade myself that something doesn't go wrong.
Which is probably me being daft. I do that sometimes.
Well, I suppose it is :P except maybe that a proposition type isn't something I usually think of as being part of higher order arithmetic proper.
Though I suppose it will happen automatically with a nullary product, so... Sure, I guess it is :P
Potentially you may have other atomic types besides N. And N isn't assumed in every treatment. Though conveniently you have completeness and soundness both with and without N.
I guess my question is, if you've got completeness and soundness for arbitrarily high orders, do you automatically get it for the n-th order fragment. Which intuitively I want to answer yes to, but I'm not sure why.
The result is that something is true in every interpretation of this higher order logic in any topos if and only if it's provable.
Lambek & Scott is the standard reference, and a lovely read.
@MaliceVidrine Well soundness of course flows downward. Completeness of course depends on what exactly you mean. But from ZC's point of view many-sorted logic (no matter the number of sorts) is trivially complete with respect to all the many-sorted models. I don't get why it matters whether it is higher-order or not.
I guess you're referring to a different semantics than I am.
Well, the usual semantics for this sort of type theory is something that's actually like the "full semantics" for higher order logics, just changing the notion of "set". With something like Henkin semantics I suppose it is a bit of a non-issue.
It's mostly nice because if you prove something about "all subsets of N" in the Mitchell-Benabou language, completeness for this semantics tells you it will be true for all subobjects of a natural numbers object in any topos, rather than there being other potential subobjects that exist in the universe of interpretation that your predicate quantifiers ignore.
(Which is what I understand happens in Henkin semantics for higher order logics.)
@MaliceVidrine Can you give me a specific example of what you mean for Henkin semantics? The standard definition of many-sorted semantics is that the model must specify the domain for each sort, so the 'higher-order' sorts may be interpreted to be objects that don't even look like 'subobjects' of the 'lower-order' objects.
Anyway I got to go now. I'll respond next time! Nice talking, and see you again! =)
So say the type of individuals is some infinite set X, and let set of "predicates" be the set of all finite and cofinite subsets of X, with the "P is true of x" predicate defined the natural way. If I'm not mistaken, this will be a perfectly good Henkin model of second order arithmetic. It's not a model of much, but clearly there are a lot of subsets of X that aren't in the domain of quantification over predicates.
The standard interpretation of the Mitchell-Benabou language in the category of sets forces the sort of predicates on X to actually be interpreted as \mathcal{P}(X).
More generally, it's always going to be the actual power object of the "sort of individuals" in an interpretation in a topos.
And the "is true of" predicate will always be what that topos understands as membership.
Er, I said a dumb thing and it's too late to edit it apparently.
When I said "second order arithmetic", that was me spacing out and typing on auto-pilot. I just meant a perfectly good structure for some second order theory.
So all I was claiming is that the intuitionistic type theory of the Mitchell-Benabou language has a semantics that is both "full"--in the sense that the type of predicates on some sort will be interpreted as the entire object of predicates on its base sort in any topos it's interpreted in--and complete. Most treatments of higher order logic paint these out to be incompatible.
Of course there's some hidden details, or sorcery, involved in this, depending on your outlook. Looking at the nuts and bolts of toposes of sheaves, one might feel that it's a stretch to call a lot of these things "predicates", or to say that certain morphisms represent quantification.
OTOH, that there is a close relationship between this higher order logic and the behavior of these objects seems to me to make a case for taking the analogies seriously....
But I'm ranting now, and I'm sleepy enough that I've lost my train of thought... :P
@user21820 - BTW, Randall Holmes agrees with me that the statement about PA proving Con(PA) implies Con(NFU) is probably true. Still working on the proof.
