Axioms - the choice & meaning

There are no three special axioms of propositional logic. There are calculi for propositional logic that have infinitely many axioms, a billion axioms, five hundred axioms, a dozen axioms, seven axioms, one axiom (e.g., [(((B -> C) -> (~D -> ~E)) -> D) -> F] -> [(F -> B) -> (E -> B)] - from Mendelson, Introduction to Mathematical Logic, 4th ed.), no axioms, and anything in between.

People might use certain sets of axioms for many reasons: convenience, elegance, custom. I imagine you usually want two things from your axioms. You want them to correspond to tautologous formulas and you want to be able to use them to prove other fomulas. Don't forget about the other part of the calculus: the set of inference rules.

Propositional logic is a two-valued logic. It only has two truth-values.

There are some 'meta-laws', you might call them, that you might want to check out. For starters, you coudl google some of these: law of the excluded middle, law of noncontradiction, principle of bivalence, law of identity.

For resources, see this: https://www.physicsforums.com/showthread.php?t=108151

Are you using a primary logic text?

 

Sorry for the sloppy post yesterday. I'm kicking myself that someone comes along who's interested in logic, and I barely say two words. Oy. Start over?

Welcome to PF, dobry_den!

I was thinking in the back of my head most of the day about how to answer these questions, and I'm still not sure where to start.

The first problem is that the best that I can offer is of course just a guess at what might have been going on in the brain of this particular author, and I suspect that's not really what you're interested in anyway. They might have borrowed this axiom-schema set from another author, which doesn't tell you much at all.

That aside, if you know what you're using the axioms or axiom schemas to accomplish, the reasons for choosing certain sets fall out naturally. Do you know what you're using the axioms to do? Creating all of the pieces for a propositional logic is easy enough that we can run through it.

You have 4 basic ingredients working together: (i) the formal, object language that contains of all of the strings that you're playing with, (ii) the semantic components that assign meanings and truth-values to strings, (iii) the calculus that generates certain strings from other strings, by certain rules, and (iv) the group of meta-somethings: the metalanguage, metatheory, and meta-whatever-else that you are actually using to define, discuss, and prove things about the other 3 parts. Are you already comfortable with each of these pieces?

 

Well, judging from your questions, the relationships among those ingredients aren't clear to you yet. Just quickly running off a list...

* You can infer a formula from the empty set of formulas, which I guess might count as a scare-quotes kind of nothing. You do need to define what a proof is, though, so you need to have at least one language before you start trying to generate proofs. Your use of 'formal' suggests that you want a formal language to boot.

* Axioms don't have truth-values, so I'm not sure what 'self-evident' means here, unless it is the definition of 'axiom'. Axioms are just formulas of your object language; they are meaningless, uninterpreted strings of symbols. This detail can be safely omitted elsewhere, but it's important here. It seems that it might have left you looking for something that isn't there.

* Axioms don't need to be basic or simple or short or anything of that sort. If you're smart, you will choose ones that will be useful to you.

* There are not merely millions, or any other large but finite amount, of calculi for propositional logic (PL) -- there are infinitely many of them. This follows at once by noting that (i) there exists a calculus for PL that has a finite set of axioms and generates an infinite set of theorems, and (ii) if C is a calculus for PL and you create a new calculus C+ by copying C and adopting one of C's theorems as an axiom, then C+ will also be a calculus for PL. You can just keep adding new axioms, creating new calculi. You can do the same with inference rules too.

* 'The three axiom schemes plus the modus ponens rule' is a calculus. (I don't know about you, but 'system' is usually what I call something when I don't know what else to call it. In case that's what you're doing, this 'system' is a calculus, given the details for replacing the axiom schemas with axioms.)

* Do you know what you want to do with the calculus, what properties you want it to have? What else could 'rightness' mean? You want semantic entailment to agree with syntactic entailment. Do you know what I mean by that?

* Well, again, formulas are just strings of symbols. They don't come with inherent, built-in truth-value assignments. The semantic components are what assign truth-values to formulas. The only truth that a formula can be said to have is the truth-value that some valuation assigns to it. You have to actually specify that a formula has been assigned a truth-value of 'true', 'false', '1', 'martha', or whatever names you choose for your truth-values.

That said, sure, you can demonstrate in an indirect way that every valuation v that assigns a truth-value of 'true' to every member of some set S of formulas also assigns a truth-value of 'true' to a formula f. For example, you can do this by proving that a proof of f from S exists in a calculus that has been proven to be sound. This is one reason for creating a calculus in the first place.

* The construction of truth tables is just an algorithm, a mechanical procedure for determining the truth-value of a formula given the truth-values of its subformulas. Truth tables are to the semantics what long division, calculators, and abaci are to arithmetic. They are calculating devices. Incidentally, in more powerful logics that include quantifiers that can range over infinite classes, the construction of truth tables for some formulas would go on forever just as a long division would go on forever for nonterminating decimals. Truth tables are of limited use.

Anywho, if that doesn't clarify things, as I said, creating all of the pieces for propositional logic is easy, so if you are willing, we can walk through each step, starting with the specification of the formal, object language.

 

Yep, it sounds that way. You could of course also define the calculus first and the semantics to match. Their 34th slide reveals the main goal: to make the set of tautologies equal to the set of theorems. This is actually a special case of a pair of theorems that we can prove soon. (One theorem says roughly that if we can prove a formula f from a set of formulas F, then f is true whenever all members of F are true. The other theorem says roughly that if f is true whenever every member of F is true, then we can prove f from F. Tautologies and theorems are the cases where F is the empty set. Anywho, we need a language first...)

I. Our Formal, Object Language L​

We get to create our own language from scratch, but to avoid all kinds of confusion, we need to clearly distinguish -- so pound into your skull the difference -- between the language that we are creating and the language that we are using to create it. The former is called the object language, and the latter is called the metalanguage.

Our metalanguage is going to be English, with some special symbols and terms added as necessary. In Klasicka matematicka logika, I imagine the metalanguage is Czech, again with some special symbols and terms added in. For short, we'll call our object language L. So

0. Our languages
(a) Metalanguage: English with some special symbols and terms.
(b) Object language: L.

To drive this home, I'll prefix meta- and L- to the relevant units for a while, starting with a correction of my first paragraph:

Yep, it sounds that way. You could of course also define the calculus first and the semantics to match. Their 34th slide reveals the main goal: to make the set of L-tautologies equal to the set of L-theorems. This is actually a special case of a pair of meta-theorems that we can prove soon. (One meta-theorem says roughly that if we can prove an L-formula f from a set of L-formulas F, then f is true whenever all members of F are true. The other meta-theorem says roughly that if f is true whenever every member of F is true, then we can prove f from F. L-tautologies and L-theorems are the cases where F is the empty set. Anywho, we need an object language first...)​

That L is a formal language (as opposed to a natural language, like English or Czech) just means that we made it up for a special purpose, it's precise, and all that good stuff. What we ultimately want from L is a set of L-formulas -- our L-tautologies and L-theorems (and L-axioms) are all L-formulas. Since L is currently empty, we need to give L some symbols. We choose the L-symbols already knowing what types of L-formulas we want to build with them. L-symbols are strung together to yield a set of L-strings, and then we choose some of the L-strings to be L-formulas. That's really all there is to it.

1. The symbols of L
(a) a countably infinite set of propositional symbols.
(b) a negation symbol.
(c) an implication symbol.

What do these L-symbols look like? We don't say. We don't care. They might not have a physical form at all. But so that we can talk about them, we give them names in our metalanguage, and for convenience, we adopt some special meta-symbols to use as shorter names. For a propositional symbol of L, we'll use the meta-symbol 'p' with indexes as needed (i.e., p₁, p₂, etc.); for the negation symbol of L, we'll use the meta-symbol '¬' (as most people do); for the implication symbol of L, we'll use the meta-symbol '→' (again, as most do).

We could of course use 'the mystery symbol of Xanadu', 'the implication symbol of L' or '$%#**bad_idea**&%' as names for the negation symbol of L, but those have some obvious drawbacks. We chose 'negation' because we intend to associate the negation symbol of L with the negation operation later on. The same goes for the other L-symbols.

2. The strings of L
(a) if l is a natural number and m₁, m₂, ..., m_l are L-symbols, their concatenation m₁m₂...m_l is an L-string whose length = l.
(b) notably, the empty string has length = 0.

So the length of an L-string must be finite, but we don't put any other bound on how long they can be. The set of L-strings is also countably infinite and includes, for example, ¬, p₁, ¬p₁, p₁¬, →¬→→p₂₃₉₅₇→→p₆₄→¬, and p₁→p₁.

3. The formulas of L
(a) a propositional symbol is an L-formula.
(b) if φ is an L-formula, then ¬φ (i.e., the L-string formed by concatenating ¬ and φ in that order) is an L-formula.
(c) if φ and χ are L-formulas, then →φχ (i.e., the L-string formed by concatenating →, φ, and χ in that order) is an L-formula.

The set of L-formulas is infinite and a subset of the set of L-strings, so it is also countably infinite. The set of L-formulas includes, for example, p₁, ¬p₁, →p₁p₂, and ¬→p₁¬p₂. And with that, L is finished.

You'll run into this same basic pattern of specifying symbols, strings, and formulas in creating other formal languages in logic, computer science, and linguistics. Though for other languages, you might have more types of symbols, different rules for strings, more steps in building formulas, and so on.

By the bye, we used only negation and implication and wrote implication formulas as →φχ in order to keep L simple. We can add meta-names for disjunction, conjunction, and whatever other shortcuts we want. We can also change the order of formulas of the form in (3c) to the more customary (φ → χ). This is just a matter of adding some definitions to our meta-language. For example, we can say

→φχ =_df (φ → χ)

and

(φ → χ) =_df (¬φ ∨ χ)

This only adds more names to our meta-language. It doesn't change L at all.

Well, there's plenty more that I could say about L and other formal languages, but I'll stop myself. Questions? Everything good so far?

(By the bye, I'm using the same basic system as is in Moshé Machover's Set theory, logic, and their limitations, 1st ed., if you want to check it out. It's one of my favorite logic books, along with Wilfrid Hodges' Logic -- and I've read dozens of them.)

 

Haha, perhaps yes, perhaps no. I might not have been as careful as I was trying to be. Just bear with me for a sec; this might be a tad painful.

Remember that saying '→' is just another way of saying 'the implication symbol of L' -- we don't know if the symbol '→' is itself a symbol of L -- we never actually write down any symbols of L. We use names to refer to symbols of L. So to be horribly precise, we could say things like 'the L-formula that "→p₁p₂" refers to' or 'the L-formulas that "→φχ" refers to', but that is a huge pain and totally unnecessary besides.*

In their normal capacity, names refer to other things. When I say that Bob is a boy with blonde hair, the string of English symbols 'Bob' refers to a boy, not to itself, a string of English symbols. To make a name refer to itself, i.e., to talk about the string instead of its referent, people conventionally put the string in quotes or italics or use some similar device (I'm using quotes), as you would do when saying that 'Bob' is a string with three letters. Putting a name in quotes takes away its normal capacity to refer. →p₁p₂ is an L-formula, just as Bob is a boy. '→p₁p₂' and 'Bob' are both strings of symbols in our metalanguage, English.

So the rules are simple:
If you're talking about the string itself, put it in quotes.
If you're talking about the thing to which the string refers, don't use quotes.

I might still bungle this occasionally, though -- let me know if you catch me. It sometimes isn't of much consequence or is presumably already clear from the context. However, sometimes it does make a difference, so returning to your question...

Yes, '(¬φ ∨ χ)' is a meta-string. Symbols in quotes should not ever be L-symbols (or L-strings or L-formulas) since we don't know what L-symbols (or L-strings or L-formulas) look like or how to write them. So '→φχ' is not an L-formula. Both '→φχ' and '(¬φ ∨ χ)' are on equal footing as meta-strings.

Yes, '(¬φ ∨ χ)' does refer to the same thing that '→φχ' refers to. They're just different names for the same thing. They both refer to a set of L-formulas (see the endnote below).

Yes, you could call '(¬φ ∨ χ)' a meta-formula, though that's a little misleading since '(¬φ ∨ χ)' contains variables and refers to more than one L-formula. Something like 'an L-formula of the form (¬φ ∨ χ)' might be less confusing.

Sorry if this was already clear to you -- I wanted to be sure. The details of the languages are perhaps the least fun parts for some, but I think that's about all I needed to say. I'll try to make time to post about the next parts overnight or tomorrow.

* Note that '¬', '→', 'p₁', 'p₂', etc. are constants; they refer to one L-symbol each. By contrast, 'φ' and 'χ' are variables; they range over the whole set of L-formulas. (These may be more specifically called 'syntactic constants' and 'syntactic variables' in order to distinguish them from other kinds of constants and variables. But you don't have to worry about that quite yet.) So '→p₁p₂' refers to a single L-formula, whereas '→φχ' refers to infinitely many L-formulas (every L-formula that begins with an implication symbol).

 

It was bothering me that I didn't have a better analogy-type explanation for what is fundamentally a simple distinction. This just struck me as I was nodding off. Let me know if it's an improvement.

Suppose that I write a paper describing all of the animals at the local zoo. Well, obviously, none of the animals are actually exhibited in the paper. If you want to see the animals themselves, you have to go to the zoo.

Suppose now that I write a paper describing the object language L. Although it might be possible to exhibit L in the paper since L is itself a language, we choose not to do this. Instead, we treat the parts of L as if they are animals in a zoo. No part of L is actually exhibited in the paper. If you want to see the parts of L themselves, you have to go to the L-zoo.

P.S. We don't say where the L-zoo is. :tongue2: Capiche?

I don't mean to keep harping on this. I'd just like to find a good conceptual hook.

 

I have a question about this,

Why do we do it this way? Why not let the symbols we draw be the actual symbols of L? Couldn't the same symbols be in both the object language and the metalanguage?

 

Sure. For example, in linguistics, when we study English using English (or Japanese using Japanese or Rotokas using Rotokas), our metalanguage and object language are the same. This doesn't make things any less complex or confusing, by the bye. By definition, whenever we study a language and our study itself takes place in a language, we have an object language and a metalanguage. Whether they are the same language or not, or whether we choose to specify any physical forms for the object language, the two roles of object language and metalanguage are still present and distinct.

When studying formal logic, the particular implementations, physical forms, or applications of the language, the shape of the implication symbol, and suchlike just aren't relevant. I imagine this is clear enough from the fact that logicians already define and study formal languages without ever specifying any of those things. You can specify them if you want to, but doing so just makes your language, well, more specific. Philosophers, computer scientists, linguists, engineers, and others can and do worry about such things. Logicians don't need to.

If you've never thought about it before, specifying a sign system -- or several of them if we want to communicate in different modes, e.g., through speech, writing, gesture, Braille, chemicals, etc. -- can be a lot of work. Even if we use existing systems, we need to define the maps between our symbols and their physical forms. Until now, I haven't bothered to distinguish between these two parts. Suppose we say that one of the propositional symbols of L has the physical form 'p₁'. Is 'p₁' the same form (does it also represent that propositional symbol)? What about 'p₁' or 'P₁' or 'p₁' or 'p_one' or 'b¹' or 'tree' or ':yuck:'? Clearly, our definition needs to be more precise, but we run into problems when we want our forms to be discrete and we have a continuous channel. We are really specifying ranges of values or clusters around norms rather than single forms (the 'single form' is another abstraction). At any rate, when specifying these things, we don't want to say that the implication symbol actually is some physical form. We want to keep the symbol separate from its form(s). And since the forms don't affect the aspects that we're interested in, we don't care what the forms are.

Also, L has infinitely many symbols. Do we want each symbol to have a unique form? Can we do that? What about for strings? Can we exhibit them all at the same time? And so on. The physical parts of sign systems, and communication systems, come with a whole new bunch of questions to answer and problems to solve -- and some answers can cause other problems. Luckily, we can shift these problems to our metalanguage and take advantage of its answers without getting the object language all tangled up in the physical world.

If you are curious, you can see some of these ideas in action, for example, in this specification of Extended Bachus-Naur Form (PDF) (HTML), a formal language developed to act as a metalanguage for specifying other formal languages. (It's used in computer science and other areas that would suffer from the ambiguities that can arise from using natural languages as metalanguages.) I'm thinking specifically about Table 1 on page 7. Notice that it lists three things: (i) the metalanguage symbol, (ii) a name for the character representation, and (iii) a glyph. For example, (i) the repetition-symbol is represented by (ii) the asterisk, which usually looks something like (iii) '*'.

 

Sorry to interject on such a productive conversation. I have little knowledge of mathematical logic, but I'm pretty sure it's accurate to say that for propositional logic at least, the original axioms were chosen because the scheme that results does make intuitive sense, i.e. the arrow of implication was intended to signify the mental meaning of "implies." Boole called his work an investigation into the laws of thought, not the laws of symbols. There are ways to specify propositional logic so that all the rules make immediate intuitive sense.

Then logicians played around with this intuitive system, and created alternate sets of axioms and rules of inference that specify the same system. The origin of the system is still that it makes sense when interpreted in a certain way.

 

Sorry, going off-topic for a moment.

Woah, you're into linguistics? Are there any forums you go to? ("... to which you go", if you're a prescriptivist.)

I love the subject, but I don't know too much about it; I've been teaching myself by picking up books on the subject and reading them, no formal basis. I'd like to learn more.

 

Hey, sorry, I haven't forgotten about this thread, just had a bad week. I'll get back to this ASAP.

 

[Note: I apologize for my crappy imitations of the symbols for logical connectives. For whatever reason, unicode isn't showing in my post preview (except for negation), and I also can't get LaTex to work. Hopefully I managed to get the message across either way.]

I think I can help with this. First, I presume that by the "three axioms of Propositional Logic," you mean what have traditionally been referred to as the "laws of thought." That is, identity, noncontradiction, and excluded middle. The reason these were called as such is that they were thought to be self-evident in the sense that they actually apply to reality and it is impossible for a human being to envision a reality in which they do not apply.

I am guessing, of course, but I would think the reason your tutor says they were chosen "independently from the (semantic) meaning of the "implication" connectives" is that, historically speaking, they were. They were chosen, depending on which development of a propositional logic we're thinking of, either because they were thought to be proved inductively through the empirical observation of the world, or they were thought to be necessary strictures on the possible ways in which a human being could conceive of logical relations.

In modern propositional logic, however, they are merely three arbitrarily chosen tautologies that are consequences of the semantic rules applied to logical connectives. They are not axioms at all, but rather are necessarily true sentences, an assertion proven by their truth tables.

Identity

p->p

Code (Text):

p p->p
T T
F T
 

Noncontradiction

¬(pA¬p)

Code (Text):

p ¬p (pA¬p) ¬(pA¬p)

T  F    F      T
F  T    F      T
 

Excluded Middle

pV¬p

Code (Text):

p ¬p pV¬p

T  F   T
F  T   T
 

These tautologies, rather than being axiomatic, arise as a consequence of the semantic meaning assigned to the connectives ->, A, V, and ¬.

However, as honestrosewater has already pointed out, the semantic meaning assigned to these connectives can be anything. It should be pointed, however, that they are not exactly arbitrary. The standard language used in modern propositional logic is meant to be translatable into natural languages. The semantic meaning of the connective A is meant to translate into English as "and." It is given the truth functional behavior it is given based on the fact that the English sentence ''Adam is a man' and 'Rachel is a woman'' is true if and only if 'Adam is a man' is true and 'Rachel is a woman' is also true. As such, the semantic meanings defined in modern propositional calculus are meant to be derivative on the naturally occuring semantic meanings of connectives in pre-existing languages. We can create other logical languages in which this is not the case, but the entire point of creating this logical language was to aid in evaluating arguments made in a natural language.