semantics(truth) vs formal system?

Question

my first question is can we just define semantics in logic and not define a formal system ?

why do we need a formal system to prove a proposition when for example we know the proposition is true ?

e.g. ( A ^ (A->B) ) -> B    if A is true and A->B is true then B is true

and this can also be shown by truth table. so why we use a formal system to show that the argument is valid when we can just use the semantics to show that . (by construction of truth tables)

since the formulas and the laws of semantics are well defined it is not possible to get to any inconsistencies (in the sense of semantics !)

i think the counterpart to my question is answered in Formal System and Formal Logical System but what about the other way around ?

my secound question is: ShyPerson when answering the above question mentioned that we need some meaning for our propositional formulas thus we define the semantics. can not we just use the same meaning of the connectives in the human language to describe our propositions . meaning we describe connectives just like the human language ?

Answer 1

Syntactic view of a Logic is the one which allows mechanical processing of formulas e.g. verifying proof or finding proofs. It describes inferences with precision that do not leave room for interpretation. You just transform formulas according to some rules.

On the other hand structure is construction of set of objects that obeys some rules e.g. axioms described by syntactic part.

For first order logic those two notions are equivalent in the sense that if you can prove something syntactically then systematical entailment will follow and other way around. This is called completeness theorem.

For higher order logic completeness theorem does not hold. Syntactic proof is sound which means that systematical entailment is implied by not every truth about structure (semantic) can be proven semantically.

Answer 2

In propositional logic we can "show" validity by truth table.

Truth table supply an algorithm to compute the truth value of every propositional formula;

in particular, truth tables can be used to tell whether a propositional expression is true for all legitimate input values, that is, logically valid [also called : a tautology].

For first-order logic, we have not a similar algorithm.

F-o logic is undecidable :

unlike propositional logic, first-order logic is undecidable (although semidecidable), provided that the language has at least one predicate of arity at least $2$ (other than equality). This means that there is no decision procedure that determines whether arbitrary formulas are logically valid.

This is the main reason why we need a deductive calculus for f-o logic :

because to show that the argument is valid when we cannot just use the semantics to show that .

Answer 3

I have the impression that it is already quite common outside logic not to care about formalization of provability but only about semantic truth. For example, when we study statements about groups or rings in our algebra classes, we do so by considering an arbitrary realization/model of the concept of group or ring inside our ambient set theory and prove the statement for all of them. Once we succeed with that, we feel the statement is 'proved'. However, what we actually did is to verify its semantic truth, and an application of Goedel's completeness theorem would be needed to conclude provability - still, this never happened to me in my undergraduate classes, and at that time I didn't even know about the precise definition of first order logic, soundness, completeness and so on.

For the foundation of mathematics, however, I think you really need logical calculi. Considering classical propositional logic, I agree that you can define a semantics through proof tables not building on any other formal system. However, when you define semantics of intuitionistic propositional logic or of first order predicate logic, you will need to explain what constitutes a set, which operation on sets are allowed, and so on. While you might do this in natural language instead of formulas, I think you will always end up with some kind of effective logical calculus.

I'd therefore say that for the foundation of mathematics, you won't be able to eliminate the introduction, either formally or on the level of natural language, of an effective proof calculus. However, once you clarified your ambient set theory through such a calculus, I agree that sometimes one can, and indeed this is often done, ignore provability and work with semantic truth.

Two final remarks:

Concerning computability, you might be interested in finding a (semi-)algorithm for checking semantic truth. Then, knowing an effective, sound and complete proof calculus for your theory will give you such a semi-algorithm for truth, and if you even know that your theory is complete (like the theory of algebraically closed fields of some fixed characteristic), you will even get a decision algorithm for truth.

Even if you don't care about logic or computability at all, there are other applications of the presence of effective, sound and complete proof calculi, for example the Lefschetz principle, or Ax's theorem.

Answer 4

There's many reasons. But one of them lies in that using a formal system can come as easier and faster than semantical system. A truth table for a proposition with 22 variables can work out as involving a lot more work than a proof of the same formula using a formal system.

Answer 5

This is more of a comment than a full answer; it's just too big to really fit well into a comment. I'm primarily addressing the question of why we don't use the connectives of natural language in logic. Besides, my ears were burning. :)

First, human languages (or natural languages) are notoriously ambiguous and vague. This makes it hard to even agree on what we're talking about.

Then come some syntactical problems. Consider the English conjunction and. In logic, conjunction is syntactically limited to conjoining just two well-formed formulas. In English, it can join most grammatical categories. Here are some examples. Nouns: Barbara and Marvin danced all night long. Verbs: Barbara sang and danced all night long. Adverbs: Barbara sang beautifully and precisely. Adjectives: The red and white ball rolled down the hill. Auxiliaries: We can and must do this proof. Clauses: Barbara walked the dog and Marvin walked the cat. And so on. I have little doubt that most natural languages allow this as well. The problem is: how do we define the semantics of the conjunction and across all these categories?

We can dodge this problem formally since we can write a different semantic interpretation for each category, but that leaves the problem that we haven't defined the core meaning of and across all these categories. And it also assumes that each category has a specific meaning. It doesn't. Consider clauses. In the example Barbara walked the dog and Marvin walked the cat, the clauses are more or less independent, like the propositional case. But how about this: Barbara drove at high speed and she parked and she got out of the car. Here the sequence is essential to the semantics: she did not get out of the car while she was driving at high speed. The propositional case doesn't represent this at all in a naive rendering; it takes work to capture in higher logics and seems quite difficult to build into the semantics of and by itself.

Now back to the need for proof. As others have pointed out, sometimes it's just not feasible to check truth tables. In fact, it's mathematically impossible, because if we could check truth tables for everything, all mathematics would become decidable. But we can't, since number theory just by itself is undecidable. "Decidable" roughly means we could write a computer program to answer every question of interest. So proof then becomes the only alternative to get to mathematical truth.

Finally, since mathematics is a science, mathematics must therefore provide scientific explanation, basically a story that helps us understand, not just a jumble of bits or numbers. I'm probably mangling this wonderful quote by Yuri I. Manin, but it goes something like this: "Proofs are understandings, they make us wiser".

Answer 6

This is to address the later half of your question. There is a limit to how far we can use connectives to give meaning to propositions. The connectives are truth functional, so they take in truth values and spit out truth values. Given that you know whether proposition A and B are true, the connective will tell you whether the proposition A^B is true, where the new proposition is made up of only the component A and B.

This is perfectly adequate if we already know whether A and B is true. But how would you know if the atomic proposition A and B is true? The connectives take the truth value of the atomic propositions as givens, but if you ask further the question of whether the atomic propositions are true, the approach of using connectives would give you no answer.

This is where you need semantics. The semantics of a formal system allow us to evaluate the truth of all statements that the formal system can express (or if you like, propositions), even the primitive ones. How does it do this? By establishing the condition under which a statement would be considered true or false. The condition that Tarski establishes is a semantical one (this is most common semantics), but there are other choices. To be clear, the meaning of the connectives is part of the semantics, but the full semantics is beyond just defining connectives.