Logic - 2018-09-05

« first day (749 days earlier) ← previous day next day → last day (2068 days later) »

6:00 AM

@famesyasd: Since you're interested in rigorous formal logic, you may want to read this post just to make sure you fully understand the stuff involved:

0

A: Do definitions have to fit axioms in logic?

Your question arises from the failure of many texts in properly distinguishing between the meta-system and the actual formal system under study. You, at all times, are doing mathematics in the meta-system, and in the field of mathematical logic you are studying some formal system (such as the one...

@LeakyNun: For the above and other related reasons, I think that people should only learn logic after they have learnt programming, where the compiler essentially forces them to understand what 100% precision means, as well as the difference between a string variable and a symbol in a string.

6:51 AM

@user21820 what is formal logic? is this opposed to meta logic?

@famesyasd Um no it's just used to refer to a 100% formal treatment of logic, as opposed to wishy-washy or handwavy vague explanations.

I mean, at some point the only way to make things 100% rigorous is to explicitly talk about string manipulation. Otherwise everything depends on the reader/listener to figure out for themselves what is what, which is of course informal.

Even the term "formal logic" itself is informal, as is any other natural language talk about mathematics. =)

In any case, all that matters is that you understand the stuff in that post. =)

7:37 AM

@user21820 Well I mean how I view it as we syntatically describe (for ex, in a computer) what a formula of our language (let's say FOL with (\in) would be like, what a proof is (<- here we also use parsing with our rules of inference (let's say your Fitch-style rules)) and also we syntatically introduce defininitorial expansion (that is we add some functions like (AddPredicate("string","formula") and then compiler checks it to be valid and if it's true id adds a new predicate symbol

to an array of our predicate symbols and a new axiom to an array of our axiom with it. And then we can go and proof all kinds of stuff like 1 + 1 = 2 or even that any function with domain {1,2,3} is of the form {(1,a), (2,b), (3,c)} that is, forall f if Function(f) and Dom(f) = {1,2,3} then exists a,b,c f = {(1,a),(2,b),(3,c)} etc If I got previous right then the only thing that I still don't understand

is what metamathemtics is about, what kind of facts we decide to be meta because not until recently I thought that that statement about functions was meta and only yesterday I discovered that I can write it down in my language and deduce it lol

@famesyasd Well, it is indeed true that you can actually do most of ordinary mathematics in a system like ZC plus on-the-fly definitorial expansion, which I will come back to later. However, in logic we often want more certainty about the theorems we prove about logic itself. In that case, we may not want to work within anything so strong as ZC.

As you can see, defining formal systems only requires being able to define a program that can perform basic operations on strings (and natural numbers). And many theorems about logic can be proven in a relatively weak meta-system MS. It is then a philosophical question. It would be terrible if you prove something about logic itself within an MS that is actually arithmetically unsound!

For example, how do we know the completeness and incompleteness theorems actually are true? It is because they can be proven in such a weak MS that we believe are sound. Similarly, the fact that definitorial expansion is safe (conservative over the original system) is a fact that can be proven in a rather weak MS.

But many logic texts never even bother to explain this, and just implicitly use the full power of ZC or even ZFC. Indeed, modern logicians and set theorists use ZFC as their MS.

And that is why you observe that practically everything you can think about can be done easily inside ZFC plus definitorial expansion.

@famesyasd Unrelated to the above, I want to say more about definitorial expansion. Your version is that if you prove some theorem (under no context) that is required for definitorial expansion, then you can create the appropriate new symbol and use it from that point onwards as if it were part of the first-order language. This is correct.

7:54 AM

yes

nice!

However one can in fact extend that to a much more practically useful version: If you prove the required theorem in any context, you can create the appropriate symbol and use it from that point onwards in that same context. (It becomes 'undefined' once you leave that context.)

@user21820 I need to go now, I have a class.

@famesyasd Ok see you!

5 hours later…

12:33 PM

dropping by as mentioned!

@user525966 Hello!

Thanks for the helpful answer on MSE

You're welcome!

@user525966: I hope the perspectives about the strings and parse trees made things clearer! Also, I wanted to say something about your question on the other answer, but the thread was already so long that I left it out.

One of your questions was:

@MaliceVidrine How do we know modus ponens and those axioms can cover any/all possible tautologies? — user525966 9 hours ago

I do some programming so treating things as strings was a helpful way to think about it

That's great!

So to answer your question that I just quoted.. In fact, that is a special property called semantic completeness. I will define it in a moment.

12:39 PM

(sorry to interrupt but I did have a quick question about semantics, before going into something that's potentially more complex like completeness)

Sure.

The semantics are completely and totally separate from the "blind strings" that compose the syntax -- when people refer to "model" are they referring to a system of semantic interpretation? Like maybe Alice's model treats "a and b" with a different truth table compared to Bob's "a and b", or maybe Dave treats "a and b" completely different altogether where truth tables don't really apply for whatever reason, etc.

When we fill out the truth table for something like $a \to b$, this is completely and totally something done on its own, i.e. we are using the truth table to define the meaning of that string?

@user525966 Correct!

or maybe Bob doesn't use truth tables at all!

@LeakyNun That's Dave.

=)

12:45 PM

oh, sorry didn't read

@user525966 truth table is the semantics of classical logic, which is one out of many systems of logic

@user525966 Right. And hence if you want to know whether a propositional sentence is a tautology or not (under the standard semantics, which is the recursive one following the truth tables), you construct a truth table with every possible assignment of (boolean) truth-values to the atoms that are relevant to the sentence, and check whether that sentence is true under every assignment.

I guess my point of confusion is how we're using axioms and inference rules if we are just making truth tables for all operators semantically anyway

truth table is the semantics

inference rules is the syntax

yeah

(I'm self-studying this for my own understanding so apologies if I am misusing terms/jargon, I'm not in a class or anything)

will probably say dumb things often

@user525966 That is where the completeness part comes in. Without axioms and inference rules, we can indeed use truth-tables to determine whether a propositional sentence is a tautology, but this method cannot extend to full first-order logic.

So let me recap a few important points.

12:48 PM

(yeah it isn't like you can determine whether a first-order sentence is a tautology)

(1) Logic was designed to enable us to have a 100% precise method of making logical deductions that are truth-preserving, meaning that if we start from true sentences we can deduce only true sentences.

Right now I'm just muddling around in 0th-order/propositional, assuming I have to fully grasp that first before moving up to predicates and such

no axioms are needed for propositional?

Yes I am stating general facts that will hold for propositional logic as well as first-order logic when you get to it.

ahh

(2) We include as axioms sentences that we believe are true under some interpretation that we are concerned about. If you are a realist, you include as axioms sentences that you interpret to assert something true about the real world.

Most logicians believe that propositional logic holds for the real world, and so any tautology holds for the real world. Note that the 'axioms' in your list are tautologies. More precisely, each of them is a schema (a list) of axioms, one for each possible choice of wffs for those variables, and each of those axioms is a tautology.

(3) We would like to have a 100% precise deductive system that can enable us to prove every sentence that is true in every model of our axioms, where "model" here means an interpretation of the non-logical symbols. For propositional logic, a model would be a truth assignment of all the atoms.

Note that (1) to (3) all depend on the term "true", which is in turn fixed by your choice of semantics.

In particular, a model M is not going to bicker with the meaning of the logical symbols, so if A and B are both true in M, then (A∧B) will also be true in M.

Makes sense so far?

1:04 PM

@user21820 what is a deductive system? rules of inference?

@famesyasd Well, most generally, it's just a proof verifier program or a theorem generator program, as I previously defined for you. But we probably shouldn't go into that technical detail right now.

The system in @user525966's question is a Hilbert-style deductive system, where there is only one inference rule modus ponens and many axioms.

@user21820 okay

There are other styles, such as my preferred Fitch-style, or Gentzen's sequent-style.

@user21820 When we list axioms and say these are true, does this mean we also must construct the semantic interpretations to match?

It seems conceivable that we make up some axioms but then end up with some mismatch in the truth tables somewhere (in theory)

@user525966 No. In general people do make up some axioms that they cannot justify to be true in any concrete sense, and there is a danger that you can indeed end up having axioms that cannot together be meaningful, or worse still that together enable you to prove a contradiction!

But for the axioms in the deductive system in your question, you can check via truth-tables that each of them is indeed a tautology.

In fact, the deductive system in your question achieves (3) for (classical) propositional logic, so we say that that system is semantically complete for propositional logic (with classical semantics).

To spell it out, that system has tautologies as axioms, and its only rule is truth-preserving, so it satisfies (1) and (2). Furthermore, non-trivially, that system turns out to satisfy (3) as well, meaning that every propositional tautology can be proven by that system!

1:12 PM

I guess I still don't understand the purpose of axioms if we're just giving operators truth tables anyway, any of those listed axioms would follow anyway

@user525966 The deductive system in your question is not permitted to use truth-tables. Is that what you're missing?

For example if I make the truth table for $p \to q$ (where it's always true unless $p$ is true and $q$ is false) then the axiom $p \to (q \to p)$ is always true / a tautology anyway, so I don't even see why we need this axiom / what we're doing with it.

chat.SE was down for me

@user525966 As I said, when you use a deductive system, you are only permitted to do what it permits. In the case of the one in your question, the only thing you can do is to apply the modus ponens inference rule to two previously deduced sentences. You are not permitted to use truth tables or whatever else.

I think we're all getting too abstract. Let's go back to Euclid's time to see what axioms mean.

Euclid derived many results of geometry using 5 axioms

1:18 PM

@LeakyNun It's not about abstractness. And Euclid was rather slipshod. He used much more intuition than his axioms...

we need to start somewhere

For me I don't understand when/where we are using modus ponens or the axioms, is my issue

As far as I can tell the truth tables cover everything

@user525966 It is true that for propositional logic, if you are allowed to use truth-tables, then you do not need any axioms whatsoever, nor do you need modus ponens.

It is no longer true for first-order logic, because you cannot extend the method of truth-tables.

let's not go to first order logic

what determines whether we are allowed to use truth tables in propositional logic or not?

There are frameworks in which they're not allowed?

1:20 PM

@user525966 on the side of syntax you have axioms, theorems, proofs, inference rules. on the side of semantics you have truth table. there are theorems linking the two sides.

@user525966 Nothing determines that, except perhaps your teacher who says "Use XXX system to prove/disprove YYY.".

The point being that, as you have noticed, truth-tables is one way that can check whether any given sentence is a tautology or a contradiction or neither.

@user525966 in particular, there is a theorem saying that the propositions you can prove using classical logic are exactly the propositions that are true under the truth table semantics

@LeakyNun Say "deductive system" not "classical logic".

Is it possible give these operators semantic meaning without resorting to truth tables?

Or is that how we define the meaning

@user525966 Well to quote from my comment:

[cont] This is not the only possible way of imbuing meaning. Given a set $X$, any assignment $i$ that maps each propositional variable to a subset of $X$ can be extended recursively to an assignment that maps each wff to a subset of $X$ according to the following: $i(¬A) = X∖i(A)$; $i(A∧B) = i(A)∩i(B)$; $i(A∨B) = i(A)∪i(B)$; $i(A⇒B) = i(¬A∨B)$. And then tautologies are the wffs that always get mapped to $X$ by the extended assignment regardless of the given $X$ and $i$. Truth-tables are not derivable, but they capture our logical intuition and motivation for logic. — user21820 8 hours ago

Specifically the last sentence.

1:23 PM

part of it too I think is not fully understand the difference between classical, deductive, etc, there are so many flavors of logic and it's a little tough to keep straight

@user525966 For now, please do not bother about other (non-classical) logics.

I agree with LeakyNun that we need to start somewhere, and I think it is best to start with the intuitive classical view of the world, where every 100% precise sentence is either true or false, and not both. That is precisely why we invented these boolean truth-values and boolean operations.

And then we can (as you did) observe that for propositional logic we can just enumerate all possible truth-assignments to analyze any given propositional sentence. So it may seem that the semantics (given by the truth-tables) already translates directly to an algorithm for determining truth.

Yes for propositional logic, no for full classical logic.

I agree; at the same time I get confused because when we talk about concepts of truth and false I immediately think of it from a programmatic standpoint, where maybe we don't talk about true and false but maybe some three-valued logic where we have [blah, bloop, blorp] instead of [true, false, neither], and suddenly we have to decide somewhere what to assign what, and my question becomes where this assignment is taking place (metalogical layer?), if this is considered a model, or a calculus, etc

I'm struggling to understand the overall hierarchy

and where the separations occur

i imagine the calculus is basically the "syntax program"

the thing telling us what correct-looking strings are like

i.e. a sentence/proposition is valid if it's generated by our calculus, and invalid otherwise

@user525966 Let's not go there yet, because you need to properly understand classical logic first before you can analyze other logics. In short, you need to work within a (classical) meta-system to analyze different logics and formal systems. Right now we are simply using natural language to explain classical logic.

and then possibly infinitely many models to interpret the strings

and all of this still being metalogical?

@user525966 One thing at a time. Right now, you don't get what is so good about a deductive system, when truth-tables suffice. I think the only real way to grasp the limited reach of truth-tables is to go to first-order logic. Don't worry, it's not hard and won't take long.

1:31 PM

I understand vaguely how to understand first order logic to the extent of for-all, there-exists, etc, and you'd have to somehow make (possibly infinitely large) truth tables to capture things, is this right?

Hmm.. sort of. But to get a proper feel of what it is like, look at (only) this list of axioms of the natural numbers. Ignore the rest of the article.

"there exists" would mean something like a_0 or a_1 or a_2 or a_3 or ..... or a_huge_number_possibly_infinitely_large = T

ok

so until then, start with classical propositional logic, that's the "walking" i must do before I can "run"?

If you understand the logical symbols, you should find that all the axioms on that list make sense, when you interpret them to be about natural numbers. Right?

when we talk about hilbert, natural deductive, sequent, etc, are these all "models" or is that strictly a semantic thing -- are these flavors considered different calculi? how are we calling these?

yes

@user525966 These are deductive systems, and are completely separate from the semantics. Some people call them calculii, but I prefer not to use more opaque terms.

1:36 PM

is every system in propositional logic a deductive system?

like is that how we're "splitting up" propositional logic as a whole?

"Propositional logic" have both syntax and semantics. Syntax includes the language (what are well-formed formulae). Semantics is the way you assign meaning to the sentences (via truth-tables). Authors differ, but I would consider deductive systems to be separate from the logic itself. That is why I said the deductive system in your question is semantically complete for propositional logic (with classical semantics).

And there are other deductive systems for propositional logic that are semantically complete too. For example, a deductive system that allows you to prove any propositional sentence such that its truth-table shows it to be true under every truth-assignment of its atoms, is also semantically complete.

But the important question that I want to pose to you is...

Is there a deductive system that can prove every sentence that holds in every structure that satisfies the axioms for natural numbers (that I just linked you to)?

i'm not sure

not even sure I fully understand what deduction even is

@user525966 In programming terms, is there a program that when run indefinitely will eventually output every single such sentence.

If you think about it, you will realize that it is a non-trivial question. So much so that Godel got his name attached to the theorem that in general there is a deductive system for first-order logic, and not just for axiomatization of the natural numbers.

And it is important to first study a deductive system for propositional logic, because it turns out that many such systems (but not truth-table methods!) can be extended to first-order logic.

every single sentence I'd suppose not

@user525966 But there is such a deductive system!

That's why I said it is a non-trivial fact.

1:50 PM

ah

Let me repeat the fact: There is a deductive system S such that, for every arithmetical sentence Q, if Q is true in every model M of the axioms in that list, then S can prove Q.

Recall that a model just has to specify the interpretation of the non-logical symbols. Over here, they are 0,1,+,·,<.

i see

To be precise, a model of these axioms must have a domain D and 0,1 must be interpreted as some elements in D, and +,· must be functions from D^2 to D, and all those axioms must be true in this model with the chosen interpretations.

Note that that list of 11 axioms is called PA− (pronounced P. A. Minus). If you add a list of axioms capturing induction, then you get PA (Peano Arithmetic).

To understand a little of the complexity of possible models, it may be instructive to look at a model of PA− that is not the natural numbers.

@user525966: Are you familiar with polynomials?

yes

Okay now consider the set P of all polynomials with integer coefficients such that either it is the zero polynomial or the coefficient of the highest-power term is positive. Now we shall define a model M with domain P and interpretation i as follows. i(0) is the zero polynomial. i(1) is the constant one polynomial. i(+) is the polynomial addition function. i(·) is the polynomial multiplication function. i(<) compares polynomials by degree first and then by its coefficients in decreasing degree.

You can slowly check that all the 11 axioms are satisfied. The first 7 are just ring axioms, so quite obvious. Axioms 8 to 12 about ordering and their interaction with addition and multiplication need a bit more thought. Axiom 13 is probably the most interesting one here.

This is just one concrete example of a model of those 11 axioms. There are other weird models, most of which cannot even be described.

To illustrate the comparison function, we would have 11 < (7X) < (X^2−4x+6) < (8X^2+5X) < (X^3−1).

Okay I got to go for a while. I'll be back later!

2:24 PM

@user21820 Could you give some examples on where this can be helpful?

2:52 PM

@famesyasd It is the same kind of helpful as the idea of using the narrowest scope as possible in programming, so as not to 'pollute the namespace'. For example, if you have a long proof, or a whole collection of proofs strung together, you may need to repeatedly use induction in multiple different contexts, and definitorial expansion would allow you to define suitable predicate-symbols, but it would be cumbersome to have to use a different variable name for each induction predicate-symbol.

Are axioms more like conveniences in prop logic?

eh I'm phrasing that wrong but I am thinking along the lines of like, being able to just know we could go from (p -> p) to (p -> (q -> p)) without needing to resort to truth tables

even though we could

@user525966 If you mean adding extra axioms to make proofs easier, sure you can add any tautology as an extra axiom.

The system in your question, however, was designed by somebody who apparently wanted a rather minimalistic system, rather than a practical one.

if we wanted strictly minimum we could get away with having just the NAND (or NOR) operator yes?

no axioms or rules of inference?

@user525966 If you have no rules of inference, you cannot deduce anything, so that would not satisfy the goal (3).

although I'm actually unsure if we can define T/F in terms of NAND alone, I think maybe

I know NAND is functionally complete but I forgot if we still need T/F somewhere

Sorry what are these 3 rules exactly / do they have a name?

3:03 PM

I didn't say they are rules; I said they are goals we want for a logic.

Again, you can look at is PA−, which you probably believe is meaningful for real-world counting. So obviously you want a deductive system that can tell you more facts about real-world counting, and not tell you any falsehoods.

And if possible you want it to have semantic-completeness, so that you know that given your axioms you will not miss out on being able to prove any sentence that is true in all the models of your axioms.

oh wow you guys are still going on

Put it another way, PA− is a (possibly incomplete) description of real-world counting numbers. You believe PA− is an accurate description, so you would like to be able to deduce all facts about counting numbers that are necessarily true given that description.

A priori (or before Godel), it is not obvious that such a goal is achievable. We know now that it is.

@user525966 And I doubt anyone has given them special names, except for "semantic-completeness" and "Godel's completeness theorem".

@LeakyNun Oh wow you're back! But I won't be going on much more; will be off again. =)

3:47 PM

@user21820 Is "logically valid" a syntactic claim?

i.e. is something only valid if it's a wff and invalid otherwise?

« first day (749 days earlier) ← previous day next day → last day (2068 days later) »

Transcript for

Sep '185

♦ $Mathematics$ Logic

This room is meant for discussion about logic, including found...

formal-systems foundations logic no-trolls

join this room
about this room

00:00

06:00

12:00

18:00

all times are UTC

$Mathematics$

site design / logo © 2024 Stack Exchange Inc; legal

mobile