@user21820 Did you know that if a relation R is symmetric and transitive then there exists a set A such that R is reflexive on A?

@famesyasd I also saw that HNQ.

Lol.

@user21820 hnq?

Hot network question.

@user21820 what is hot network? this is where? on mathstackexchange?

oh I think I see

@user525966 No. What made you think so? The definition of "logically valid" varies, but in general always refers to validity in all models. So we might say that an inference rule is logically valid, to mean that no matter what sentences you apply it to, if they are true in a model M then what the inference rule allows us to deduce is also true in M. But I try not to use this term when I'm being precise.

@user21820 Is there a reflection principle for first order ring theory

@LeakyNun What is a reflection principle?

i.e. for every sentence phi there is a ring R such that (phi is true in every ring) iff (phi is true in R)

Hmm something must be off about your claim. For every sentence Q either it is true in every ring or it is false in some ring, and either way we can pick a ring R according to which case it is.

but is there a formula for picking R?

@LeakyNun Formula in where? In any reasonable system that can talk about rings and knows the existence of at least one ring, it would be trivial, since in the first case you just use the ring you know, and in the second case you just use a ring that does not satisfy the sentence Q. In the second case, the ring axioms plus (¬Q) are consistent because they hold in some ring, so I think you only need something like WKL to be able to construct a distinguished countable model (leftmost branch).

In ZFC you can just whack with AC.

I’m using the informal usage of formula

like, is there an algorithm

@LeakyNun Well, WKL is non-computable.

So I guess you want to know whether rings are sufficiently nice.

@LeakyNun And now I don't understand your question. What does it mean to have an algorithm whose output is a ring?

@MaliceVidrine: Hello there!

Yo

Been a minute since I popped in one of the chats, and I saw the link and was bored... :P

So, what's new in here?

Ah. =)

Hopefully this is helping 525966. I kept trying to move a comment thread here the other day but m.se wasn't having it.

@MaliceVidrine I think my answer did clear up the syntax issues, because it's true that it is either a technical error to use the equality sign when defining new notation, or a pedagogical problem.

And I also briefly introduced the semantic-completeness question to user525966 after that.

Yeah, it seemed that much of their confusion was how syntax and semantics are related.

And equality in that context is, I think, terrible pedagogy. :P

@MaliceVidrine Anyway, if you're bored, you can try a puzzle I came up with.

So far, everyone who has solved it (only 3 including myself) has given a different proof...

Hm, interesting. Exactly the kind of problem I'm terrible at :P

Getting out the notebook....

hi guys

Yo.

Anyone knows about logic of mpin, how does it work

@MaliceVidrine On the topic of pedagogy, I think Hilbert-style deductive systems are terrible. It makes little sense how the axioms are devised unless you already understand logic well enough or are familiar with a Fitch-style system. And it's even more terrible to define nice familiar operations like ∧ and ∨ in terms of ⇒...

Of course, Hilbert-style systems are simple for analyzing from the outside... But a first course in logic shouldn't use them, in my opinion...

@krishnamahadik Mathematical logic does not study MPIN. Please read the room description. =)

oops, Sorry guys..

@user21820 - Agreed. I weep for people I see assigned proof exercises using a Hilbert proof system. Even proving P -> --P was, IMO, a grim experience when it should be a triviality.

As I've learned more I've really come to appreciate Gentzen-style proof systems.

@MaliceVidrine When I was first given that exercise, it took me a while. And that's despite having already designed my own Fitch-style system...

I mean, if you start dealing with fragments of logic without implication or universal quantification, sequent calculi are just about the only half way sensible way to deal with them.

Are hilbert systems those where you have modus ponens rule and a lot of axioms?

Yep

They are a joke

@famesyasd And Gentzen-style systems include LK.

It took me a long time to like LK. I now attribute this to bad taste and immaturity ;P

@MaliceVidrine Technically, Fitch-style systems are as flexible as sequent-style systems, although admittedly troublesome to formalize. For example it's easy to capture the most common modal logic of necessity and possibility using a Fitch-style system where one possible context is the ⬜.

Unfortunately, I haven't seen/found a deductive system for classical logic that both has the nice symmetry of LK and the pragmatic elegance of Fitch-style (little unnecessary repetition).

Incidentally, I don't suppose you have a helpful comment on my bountied question? I realize it might be a pretty trivial question, but I still don't trust myself not to have missed something silly :P

what is mpin?

@MaliceVidrine I am not familiar with Heyting logic/categories, sorry.

@LeakyNun I didn't know either, and googled it.

Ah well. I'm trying to study intuitionistic models of a certain theory, and it looked like classifying toposes might be an angle on it. But the theory itself is very much not coherent in its default form, and now it looks like the "coherentization" may never be properly intuitonistic. Which is just a bummer.

I should listen to Forster and Holmes and stop fiddling with the topos theory, but it's just so pretty...

Hahaha..

@famesyasd: How about you, have you figured out my pretty puzzle? =D

I see a pattern in the puzzle, but now I need to figure out a real proof...

@user21820 nooo, as I said I have solve a line case based on some invariant and then tried to generalize it to the circle (basically I cut a cricle to the line to define once again left adn right there) but it failed for the odd number of colours but t works for even, I think, and it almost works for the odd numbers too but there are some positions that my necessary condition does not cover so I left it there

@famesyasd What is the proof you had for the line case?

@user21820 Let's say you have green stones and then red stones, you compute the parity of number of red stones which have odd number of green stones to the left of them, and then check that this number's parity is invariant but in the beginning you had it odd and after replacement it gets even...

Huh. Did stackexchange just suddenly remember the icon I uploaded a while back?

@famesyasd Okay that works. Great! Yes the circle version is harder.

All right, sleep it is. Until next time.

@MaliceVidrine Ok see you!

@user21820 I guess I am just confused over definitions

How exactly do we define a premise and conclusion? Is it the same in any logical system?

I typically see it $\text{premise} \to \text{conclusion}$ but $\to$ in itself can be defined however we want it so I'm a little unclear if there is a stronger claim that we can make from a metalogical level

@user525966 Isn't it related to the construction of wff?

@user525966 The use of "→" or "⇒" as a symbol that is inside first-order logic is merely a symbol called implication, and its meaning is (as discussed above) given by the standard interpretation of first-order logic, which means the truth-table for implication. There is no 'claim' to be made. Given any sentences A,B, we can call A+"→"+B a conditional sentence with condition A and consequence B.

I have a general distaste for texts that talk about "proofs" as having "premises" and "conclusions", because their explanations are usually problematic, and the notion of "premises" is quite outdated. Just know that "proof" is always tied with a deductive system, and for classical logic (which is our concern), there will be axioms and inference rules. Recall the axiomatization of PA− that I showed you. We chose those axioms because they seem true when we interpret them to be about naturals.

Now to obtain more true sentences about naturals, we use inference rules. I give one possible Fitch-style deductive system for first-order logic here. You should actually try it out to see how logical reasoning can be done with 100% precision yet in a reasonably human-friendly manner.

As I said, there is no need to talk about premises and conclusions. If you want to do 100% formal simple number theory (over PA), you can use the axioms (with the induction axioms) and the deductive rules in my post.

Then whatever you can prove under no context is a theorem of PA.

Similarly, a 1-parameter sentence over PA is just like a sentence except that it can also depend on a parameter. For example Q = ( p ↦ p>1 ∧ ∀k,m∈N ( k·m=p ⇒ k=1 ∨ m=1 ) ) denotes a 1-parameter sentence over PA where the parameter is denoted by "p". To check your understanding, observe that in the intended interpretation (where N is the naturals and 0,1,+,·,< have the standard arithmetical meaning), Q(p) is true for p∈N if and only if p is a prime.

Now the induction schema can be described. For each 1-parameter sentence P over PA, PA has the axiom "P(0) ∧ ∀k∈N ( P(k)⇒P(k+1) ) ⇒ ∀k∈N ( P(k) )". For example, for the 1-parameter sentence E = ( p ↦ ∃x∈N ( x·2=p ∨ x·2+1=p ) ), PA has the axiom "∃x∈N ( x·2=0 ∨ x·2+1=0 ) ∧ ∀k∈N ( ∃x∈N ( x·2=k ∨ x·2+1=k ) ⇒ ∃x∈N ( x·2=k+1 ∨ x·2+1=k+1 ) ) ⇒ ∀k∈N ( ∃x∈N ( x·2=k ∨ x·2+1=k ) )".

Of course, since there are infinitely many 1-parameter sentences over PA, PA will also have infinitely many induction axioms. That is why it is called a schema (list), because it is not a single axiom.

@user525966: A good exercise would be to actually prove "∀k∈N ( ∃x∈N ( x·2=k ∨ x·2+1=k ) )" in the Fitch-style deductive system. Hint: Use that particular induction axiom I just wrote out.

By the way, I am being a bit imprecise in my description of 1-parameter sentences because it is troublesome to give a 100% precise syntactic definition. If you have any clarification questions, go ahead and raise them.

I'm trying to get the basics before I jump into first-order stuff, which seems a lot more complex

@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 )".

@user21820 Prove in what sense?

A or not-A is either (0 or 1) = 1, or (1 or 0) = 1, so true either way, or is there some other way we're meant to prove such things

@user525966 what did you try to prove in your last example?

A or (A -> B)

user21820's previous comment

'Two exercises you can try are to prove "A or not A" and "A or ( A implies B )".'

@user525966 I see, can you prove (A and B) -> (B and A)?

@user525966 - The suggestion was to try proving it using the deductive system that @user21820 linked to, not just doing truth tables.

@MaliceVidrine Not sure what that really means

Have you looked at the link?

Yeah but they seem more of a first-order thing which is more advanced than what I'm trying to understand at the moment

Trying to stay with prop logic

Don't really understand what this Fitch stuff is used for or why we need it for this

Your questions give the impression that you're interested in the idea of proof, and how proofs work. If you're not, then I suppose you don't need it.

I'm interested in all of it

but I still want to understand it and how it works

I don't like rote memorizing

The point is not rote memorization, the point is to actually engage with an example of a proof system so you can understand what it's doing.

How does a proof system fit into the greater context of all this

In what sense does it relate to axioms, or a logic system, inference rules, truth tables, etc?

I can't tell how many modular parts there are to all this logic stuff

Which things apply to all systems, how they're organized, which aspects can be swapped around, etc

That's because you're trying very hard to understand an entire field of mathematics at once, which you're simply not going to pull off. You presumably wouldn't go into another area of math and try to understand what's a derivative, what's a differential equation, how does it relate to Galois theory, or linear algebra, etc. and expect someone to clarify all of this in a few questions-answer sessions.

A proof system for a particular logic is the collection of rules of inference and axioms.

I don't suppose you've ever encountered Turing machines or register machines, since I recall you saying you have more of a programming background?

only vaguely, heard of them but never messed around with those formally

An analogy probably won't clarify anything, then....

My issue is that whenever we talk about anything in logic I can't tell if it's a concept that only applies to a couple specific systems, or all systems, or systems of a certain flavor, what those flavors are, and so on

first I learned we had different orders of logic, and then within 0th order (prop logic), there are different varieties (hilbert, ND, intuitionistic, sequent), and then different "interpretations", different axioms, different inference rules, different proof systems, metalogic and logic, syntax and semantics, etc

I know, and you're not going to learn that all at once. So just try to understand some basic cases.

I know this stuff has answers but it's just not organized online in any sort of clear way

The spirit of a proof is that you imagine you have a sheet of paper, with some initial formulas written down on it. You have some rules that say what you're allowed to write down on each line, given the contents of the prior lines. Modus ponens is just this kind of rule: if you've already written down P in a prior line, and you've written down P->Q, then you can write down Q on the next line.

right

that's exactly how I picture it too

i don't know if it's accurate or not but I literally think of it as "we can write it down on the paper"

if we've written P and P->Q then modus ponens says we can add Q as another formula

but then this causes me confusion

because wouldn't we need to know what Q is in order to write P->Q in the first place? What does it even really mean to be able to write it down?

if we're doing this in terms of syntax rather than semantics

i.e. not making any claims about truth value yet

i.e. what are we actually saying simply by writing something down on the paper (we could write anything down if we wanted to)

If you don't know what the letter Q is, or how to write it, then you have bigger problems :P

I'm talking about what it represents, not just the letter itself, haha

That's entirely irrelevant to the idea of proof.

@user525966 Forget about truth and semantics

@user525966 In the beginning we only have purely syntactic things

yes

If your issue is that it seems like we could define nonsensical proof systems without some idea of what we're trying to put on paper, the answer is yes, we certainly could.

I'm asking "what is P, P->Q $\vdash$ Q" really saying

But we have an idea of what we're trying to put to paper, so we design proof systems that seem to behave like the thing we intuitively have in mind.

It's saying "if you start with the lines P and P->Q on our paper, then the rules let us write down Q."

and what lets us write P and P->Q on the paper in the first place? the axioms?

The definition of a well formed formula.

wff's appear to be generated recursively and end up covering all possible formulas that could be constructed

Well, it's more like they're the class that we want to define "possible formulas". We want to exclude things like "P->)->" that just don't look anything like the kinds of strings we want to use.

@user525966 "P" and "P->Q" are some sentences in some formal language that you designed yourself. Like C or C++. It is YOU who decide what meaning they should have

yes, I do understand all that

Okay so the idea is that you write down and manipulate those strings in that formal language by the rules (of logic) and you decide yourself what logic rules you want to have and then you interpret the results (strings) that your receive into real world

But yes, they are recursively defined, by clauses like "atomic sentence letters are WFFs; if P and Q are WFFs, so is P & Q.... etc." Or at least this is the case in the logics we like to study.

yes

and once again HOW you decide to interpret those strings into real world all depends on yourself, basically it all comes the agreement like all people agree that this and this string means this and this thing

the way in which we choose to interpret

how do we describe that?

a semantic interpretation system?

(or some other phrasing?)

@user525966 Intuitively

So the assignment of true and false to well-formed formulas, based on their syntactic structure, is the semantics for propositional logic. For first order logic, the usual semantics are Tarski models.

But let's focus on propositional logic, obviously.

I mean do we just call it the semantics?

ok

As a contrast to "the syntax", then yes, we'd just call this feature of the logic "the semantics".

In the propositional case, formally speaking, an interpretation is just a function from the set of formulas to the set of truth values, with the structure imposed by the familiar truth tables.

So inferences in general, do they differ depending on the system?

in terms of what they're accomplishing?

P, P->Q ⊢ Q -- this just means Q is provable from P and P->Q but I guess I don't really understand what this means

You mean different proof systems for the same logic?

I guess just trying to understand if "inferences" work the same way in all logics

i.e. do most systems use modus ponens as their inference rule?

No, not all. Or at least, they don't all use it as one of the basic rules.

For propositional logic, the various proof methods -- Gentzen, Hilbert, Fitch, etc. may use different basic rules, but they'll all be able to prove the same things.

There are some logics, that are usually only studied for very particular purposes, that don't have "->" as one of their logical symbols, so modus ponens doesn't make sense there, but that's a rather special case.