Definitions in terms of truth-functions

[honestrosewater]

In another thread, I started to say that "tautology" and "contradiction" could be defined in terms of truth-functions- which seemed entirely plausible- but I can't figure out how to do it. A tautology is a proposition whose truth-value is always Truth (T); a contradiction is a proposition whose truth-value is always Falsehood (F). To give you an idea, I first tried: A proposition D is a tautology if, for any contingent proposition P, (D & P) <=> P. A proposition C is a contradiction if (C v P) <=> P. But these use "<=>" which means the proposition is a tautology! -so that won't work. ((D & P) <-> P) <-> ((C v P) <-> P) <-> D and (P v ~P) <-> D and (P & ~P) -> D etc. don't work because they're contingent and the definitions need to be tautologous. I can certainly build tautologies out of contingent propositions and connectives, but I need to figure out if I can build a definition that way. Any thoughts?

 

[BicycleTree]

What are you trying to do?

A tautology is a proposition whose truth-value is always Truth (T); a contradiction is a proposition whose truth-value is always Falsehood (F).

Sounds OK to me. You also say that D is true and after reversing the truth value of any number of variables in D, D is still true. You could also say that D can be derived without premises. If Dx is a composite statement in propositional logic, you could define a universe of objects such that every atomic formula that is part of Dx is true for some object and false for some other object, and say Ax(Dx) where Ax means "for all x."

What is the difference between <=> and <-> as you are using it?

 

[honestrosewater]

What are you trying to do?

I'm not sure how else to explain it. I'm trying to find a proposition in a formal language for propositional logic which I can use to define "tautology" or "contradiction". I know there are several ways of stating the definitions; I am looking for this specific way.

What is the difference between <=> and <-> as you are using it?

"<->" denotes regular equivalence; "<=>" denotes logical equivalence; When (P <-> Q) is a tautology, P and Q are logically equivalent. IOW, (P <=> Q) means P and Q are equivalent for all truth-value assignments to their atomic propositions.
So my first attempt:
A proposition D is a tautology if, for any contingent proposition P, (D & P) <=> P.
which seems to work as a definition of tautology, is a hollow victory unless I can define "<=>" without using tautology.

 

[Hurkyl]

I'm not sure just what you're trying to do...


My interpretation of what you've written makes me think you're doing something that doesn't make sense: propositions in a given language cannot speak about other propositions in the same language. If they could, you quickly run into the Liar's Paradox.

Of course, a proposition in second-order logic can talk about propositions of first-order logic... is that what you're trying to do?


I'm just really confused about what you're trying to do.

 

[BicycleTree]

Note: I elaborated on that suggestion of the universe of objects, then deleted it because it was incorrect and forgot to put a reason for deletion.

 

[honestrosewater]

Okay, sorry. I just want a proposition in a formal language L for propositional logic which I can put into an English sentence to make the English sentence a definition of tautology. For instance, the English sentence:
"(P v ~P) is a tautology."
contains the proposition "(P v ~P)" which denotes, for all intents and purposes, a proposition in L; Say, because I defined L to have an infinite set of propositional symbols which I chose to denote by capital Enlgish letters, adding subscripts when necessary, etc. So I just want to find a proposition in L to fill the blank in the English sentence (or something like it):
"A proposition in L is a tautology if [blank]."
I tried:
"A proposition D in L is a tautology if, for any contingent proposition P in L, (D & P) <=> P."
Here, the proposition in L would be "(D & P) <=> P", however that particular proposition won't actually work because, even though it says that D is an arbitrary proposition in L whose truth-value is always T, (Edit: Eh, it says that in my definition, I mean.) "<=>" is not a symbol in any L that I know of, and I don't know how to include it in L since it would most naturally be like a truth-function but isn't a function from {T, F} to {T, F}. Secondly, in English, "<=>" is defined using tautology. So even if I wanted to include "<=>" in L, in order to define "<=>" in L, I would probably have to first find the very proposition in L for which I'm searching: a proposition in L which I can basically use to denote the set of all tautologies in L. I don't know- does that help?

 

[Hurkyl]

a proposition in L which I can basically use to denote the set of all tautologies in L

As I mentioned before, this can't happen. The usual system of formal logic is designed specifically so that such self-reference is not possible, because you quickly run into the Liar's paradox.

 

[honestrosewater]

As I mentioned before, this can't happen. The usual system of formal logic is designed specifically so that such self-reference is not possible, because you quickly run into the Liar's paradox.

Okay, let me start over because I don't see how that applies to what I'm trying to do.
Let M be a formal language containing
1) a number symbol, denoted by "x",
2) an operation symbol, addition, denoted by "+", and
3) an equation symbol, denoted by "=".
Expressions in L are defined as follows:
4) "x" is an expression.
5) If x is an expression, "x + x" is an expression.
Equations in L are defined as follows:
6) If x is an expression, "x = x" is an equation.
So (6) defines an equation, and "x = x" denotes the set of all equations in M: {x = x, x + x = x + x, x + x + x = x + x + x, ...}. That's all I want to do- but for a different language.
Let L be a formal language containing
1) an infinite set of propositional symbols, and
2) two connective symbols, or and negation, denoted by "v" and "~", respectively.
A propostion in L is a finite string of propositional symbols and connective symbols, contructed by the usual rules.
Let "P_n" range over the set of propositions in L (dropping the subscript when convenient). Then "P v ~P" denotes a subset of the set of all tautologies in L (adding parentheses for grouping): {P v ~P, (P₁ v P₂) v ~(P₁ v P₂), (P₁ v ~P₂) v ~(P₁ v ~P₂), ...}.
That's all I want to do. It's not really a big deal, I'm just wondering if it can be done for all tautologes in L. Since it can be done for a subset of all tautologies in L, it seems plausible. In fact, perhaps all tautologies in L can be written in the form "P v ~P". I guess that's the first thing I'll check.

 

[Hurkyl]

Ok, I think I follow what you're trying to do.

P or ~P won't work, because the tautology ~(P and ~P) isn't of that form... and neither is ~~(P or ~P).

In fact, for any finite collections of these forms, I conjecture that you can find a tautology not of one of those forms simply by taking your favorite tautology and tacking on a sufficient number of double negations.

 

[honestrosewater]

P or ~P won't work, because the tautology ~(P and ~P) isn't of that form... and neither is ~~(P or ~P).

"and" isn't a connective in L- only "negation" and "or"- which do form an adequate or complete set of connectives. There are no parentheses in L either- I just added them for familiarity. So "P v Q" would be written "vPQ". Actually, here's the definition of proposition, or formula, in L:
1) a propositional symbol is a formula.
2) If P is a formula, ~P is a formula.
3) If P and Q are formulas, vPQ is a formula.

In fact, for any finite collections of these forms, I conjecture that you can find a tautology not of one of those forms simply by taking your favorite tautology and tacking on a sufficient number of double negations.

Okay, my test formula is "vP~P", where "P" ranges over formulas. So ~(P & ~P) would be "vP~P", where P denotes the formula "~P". But now I see order is a problem. I could define a primitive or simplified standard form, where, say the formula of least length goes on the left, so that "v~PP" would be a derived form of "vP~P". Or whatever. But your double negation is a harder problem. I think my original expectations are out the window, but perhaps I could define tautologies in a finite number of steps, following the construction of formulas:
1) If P is a formula, vP~P and v~PP are tautologies.
2) If T is a tautology, ~~T is a tautology.
3) ?Any more forms?

 

[Hurkyl]

Here's a simple algorithm for printing out a list of all tautologies:

For each possible formula:
- Compute all possible truth assignments for the variables
- If they're all true, print this formulae


We can iterate through formulae by, say, going through all propositions of length 1, then of length 2, etc.


Alternatively, mathworld says that every tautology has a formal proof in propositional calculus.

So, one could just encode the axioms and rules of deduction of propositional calculus as a "string rewriting" rules, like "2) If T is a tautology, ~~T is a tautology." and you'll have what you seek.

 

[honestrosewater]

Here's a simple algorithm for printing out a list of all tautologies:

For each possible formula:
- Compute all possible truth assignments for the variables
- If they're all true, print this formulae


We can iterate through formulae by, say, going through all propositions of length 1, then of length 2, etc.

Okay, but there are an infinite number of formulas. Their lengths range over the nonnegative integers.

Alternatively, mathworld says that every tautology has a formal proof in propositional calculus.

So, one could just encode the axioms and rules of deduction of propositional calculus as a "string rewriting" rules, like "2) If T is a tautology, ~~T is a tautology." and you'll have what you seek.

Oh, you're great- theorems and proofs. And there are even axiomatizations with only one axiom schema and one inference rule- beautiful! I started wondering why I had never seen anyone define tautologies this way- but they have- and it was right in front of me the whole time. Well, I haven't actually gotten to axiomatizations yet, but still- so much to learn. Thanks- I can't explain how beautiful that is.

 

[Hurkyl]

Okay, but there are an infinite number of formulas. Their lengths range over the nonnegative integers.

Yep, but the important thing is that the length of any individual formula is finite, and there are only finitely many distinct formulae of each length. (By distinct, I mean that we consider ~P and ~Q to be the same formula, since it's simply a relabelling. We would still consider vAvBC and vvBCA different formulae, though)

So, this algorithm will list every tautology, and we can use it as a decision procedure, because we can tell where any given formula should have appeared in the list.



There are so many definitions that turn out to be equivalent that my head spins and I forget which is which. But one of the points is that it's not obvious from the outset that "A proposition that is true for every assignment of its variables" is equivalent to, say, "A proposition that follows from the empty set of premises", nor to "A proposition that holds in every model of propositional calculus".



Anyways, you're beginning to touch on computability theory, I think! You have this sublanguage T of L consisting of all the tautologies.

If I understood your question properly, your goal seemed to be one of the two following:

(1) You wished to find an algorithm for enumerating T -- that is, print out a list of all tautologies.

(2) You wished to find an algorithm for deciding T -- that is, given a formula, to tell whether it is in T or not.


The first is equivalent to asking about Turing recognizability -- is there an algorithm that, when given something in L, will eventually halt and say "yes" if it's in T, and will never say "yes" otherwise.

The second is equvialent to asking about Turing decidability -- is there an algorithm that, when given something in L, will eventually halt and either say "yes" or "no", depending on whether or not it's in T.


IIRC, Turing recognizability is equivalent to the idea of string rewriting -- the class of languages you can recognize with an algorithm is equal to the class of languages you can produce via string rewriting.

Anything decidable is, of course, recognizable.

Because of all this, to answer your question, it was sufficient to provide an algorithm that can tell if a given formula is a tautology or not.


(As you might guess, I learned a lot more about this sort of thing from my computer science courses than my math courses!)

 

[honestrosewater]

Yep, but the important thing is that the length of any individual formula is finite, and there are only finitely many distinct formulae of each length. (By distinct, I mean that we consider ~P and ~Q to be the same formula, since it's simply a relabelling. We would still consider vAvBC and vvBCA different formulae, though)

So, this algorithm will list every tautology, and we can use it as a decision procedure, because we can tell where any given formula should have appeared in the list.

Ah, I didn't see that as a decision procedure. I get it now.
Speaking of lots of definitions, let me get a few things straight very briefly. We have semantic entailment and syntactic entailment. Semantic entailment is associated with a decision procedure, say truth tables, and theorems. Syntactic entailment is associated with a proof procedure (axioms, inference rules), say natural deduction, and proofs. For soundess, syntactic entailment (there is a proof of P in L) implies semantic entailment (P is a theorem of L). For completeness, semantic entailment (P is a theorem of L) implies syntactic entailment (There is a proof of P in L). I really don't want to mix this up. Edit: I'm actually asking if I've got that all right; I know you know what completeness means.
So, basically, personally, when I have something I want to check, I think semantic; When I want something I need to construct, I think syntactic. But what you say below confuses me- but in an encouraging not frustrating way.

Anyways, you're beginning to touch on computability theory, I think! You have this sublanguage T of L consisting of all the tautologies.

If I understood your question properly, your goal seemed to be one of the two following:

One thing, very quickly: Say I want a definition of an even number- I pick a test equation. I have a variable in my equation so that if I plug in a number, and the equation is true, then the number is even; IOW, it doesn't accept any uneven numbers. Also, if a number is even, and I plug it into my equation, then my equation is true; IOW, it doesn't reject any even number. This is what I was after, initially. It seems to fit the 2-part semantic/syntactic distinction (there is a proof of P in L ~ my equation is true, and P is a theorem of L ~ the number is even, I think). In fact, how else but by having both could you check that both requirements are met? (And have it somehow be not circluar too?) Anyway, you seem to say below that one of them- the equation accepts only even numbers, or the equation accepts all even numbers- implies the other. But 4n = x (only) and n = x (all) -and a little thought- seem to say otherwise (x being the variable of interest and n natural). So I've misunderstood or it doesn't apply here.
Actually, I just realized how prevalent that idea of all and only is, even all and only, separately. Maybe just because they're in definitions and set theory. Okay, shutting up.

(1) You wished to find an algorithm for enumerating T -- that is, print out a list of all tautologies.

(2) You wished to find an algorithm for deciding T -- that is, given a formula, to tell whether it is in T or not.


The first is equivalent to asking about Turing recognizability -- is there an algorithm that, when given something in L, will eventually halt and say "yes" if it's in T, and will never say "yes" otherwise.

The second is equvialent to asking about Turing decidability -- is there an algorithm that, when given something in L, will eventually halt and either say "yes" or "no", depending on whether or not it's in T.

So I want to associate enumerating with syntactic entailment and proofs; Deciding with semantic entailment and theorems. Is that right?

IIRC, Turing recognizability is equivalent to the idea of string rewriting -- the class of languages you can recognize with an algorithm is equal to the class of languages you can produce via string rewriting.

Anything decidable is, of course, recognizable.

Because of all this, to answer your question, it was sufficient to provide an algorithm that can tell if a given formula is a tautology or not.

These two confuse me because of the connections I've made (bear w/ me please):
1) deciding ~ decidability ~ semantic ~ P is a theorem ~ x is an even #
2) enumerating ~ recognizability ~ syntactic ~ a proof of P ~ a true equation for x
3) soundness ~ syntactic -> semantic ~ accepts only
4) completeness ~ semantic -> syntactic ~ accepts all
Then decidable -> recognizable would mean -oh, I think writing that out just cleared it up ;) - it would mean the system was complete? (I was thinking it meant completeness implied soundness which was wrong.)
But telling "if a given formula is a tautology or not" I would connect to "accepts only", i.e., being sound. So I'm still a bit confused; I can't put it all together, and I'm not sure I'm good so far.

(As you might guess, I learned a lot more about this sort of thing from my computer science courses than my math courses!)

Well now I'm looking forward to computer science classes! I thought they would be mostly application.

 

[Hurkyl]

I'll be honest -- this stuff was only in one computer science class: "Theory of Computation". However I've picked more up from literature.


Anyways, I'm the wrong person to ask about the technical details about definitions and stuff. But going from:

"Semantic entailment is associated with a decision procedure"
"Syntactic entailment is associated with a proof procedure"

Then your first paragraph looks right... except possibly your use of the word "theorem". I thought the definition of theorem was a statement that has a proof! I could easily be wrong, though.




Let me restate the meaning of recognizability and decidability:

A recognizer for a language L is a black box that accepts a string as an input, thinks for a while, and says "yes" if and only if that string is in L.

A decider for a language L is a black box that accepts a string as an input, thinks for a while, and says "yes" if and only if that string is in L, and "no" if and only if that string is not in L.


The difference between a recognizer and a decider is that the decider comes with a guarantee that it will eventually finish thinking and give you an answer. The recognizer only provides a partial guarantee -- if the string is in L it will stop.

So, functionally, a recognizer cannot be used to tell if a string is not in the language L. Even if we wait 10 years and the recognizer hasn't given us an answer, we still don't know if it will stop and print "yes" tomorrow or keep on going forever!


The interesting types of recognizers and deciders are Turing machines. If a turing machine can act as a recognizer a language, it's called turing recognizable, and similarly for Turing decidable. These are interesting because, by Church's Thesis, "there's an algorithm to do ..." is equivalent to "there's a turing machine that does ...".


Incidentally, languages that can be recognized or decided via string rewriting are called recursively enumerable and recursive, respectively. As I mentioned before, they are equivalent to turing recognizable and turing decidable, respectively.



There's an interesting turing machine that does the following: given a statement, it goes through all possible proofs looking for one that proves either the statement or its negation.

This machine always acts as a recognizer for the language of statements that can be proven in a given theory. (Well, there are some restrictions on the theory -- I guess it would have to be axiomized by finitely many schema, or something like that)

However, if the theory is both complete and complete, that is every statement is either true or false, and all true statements have a proof, then this machine acts as a decider for it. The converse is also true.

 

[honestrosewater]

Then your first paragraph looks right... except possibly your use of the word "theorem". I thought the definition of theorem was a statement that has a proof! I could easily be wrong, though.

If we go by mathworld, you're right and I meant tautology instead of theorem. (But part of their definition of tautology is "A logical statement in which the conclusion is equivalent to the premise..." which doesn't really make sense to me, but the equivalency part is wrong on any reading I can think of.)

Let me restate the meaning of recognizability and decidability:

Okay, I get it. When you said anything decidable was recognizable, I was thinking of strings instead of languages (where a string is blankable in L iff it makes a blanker for L halt). This makes sense for languages. For strings, being recognizable implies being decidable, but the converse fails. Right?
I'll have to play around with the rest. I think I pretty much understand all of the pieces, I just need to put them together. This is great stuff BTW, I really appreciate it.

 

[Hurkyl]

Heh, I never thought of the definitions in terms of a single string before!

No, I don't think they have any meaning for a single string S -- recognizers for a language are not unique. Once you've chosen a particular recognizer, you can then ask if it halts on S. But given S, there will always be a recognizer that halts on S. (And if S is not in the language, there is always a recognizer that fails to halt on S)

 

[honestrosewater]

Okay. I was basing that on the other half of the definition: S being in L or not.

I've got part of it together. We define a set of formulas X in language L. To get a set of tautologies Y in L, we define a truth-valuation on L (a mapping from X to {T, F}). To get a set of theorems Z in L, we define a set of axioms (a subset of X) and a set of rules of inference. These last two sets are called a calculus. Our calculus is sound and complete iff Y = Z. But I think that for every Z, there is a truth-valuation such that Y = Z, and for every Y, there is a calculus such the Y = Z, because we can define the truth-valuation and calculus however we want. If Y (or Z) is finite, we can just list the axioms (or truth-values) accordingly. I'm not sure about when Y or Z are infinite- I'll have to learn more, but I know it's true for some cases.
Anyway, I wanted a finite set of "formula schemas" that I could use to define tautology. When this is possible, those schemas are now obviously the schemas used in the axiom set or in the truth-valuation. The calculus acts (or could act, with whatever modifications needed) as a recognizer for Z, and I can (in at least some cases) define the truth-valuation to make Y = Z. The truth-valuation acts as a decider for Y, and, well, Y is the set of tautologies. Sound good?