Logic

• "Entails"
  • means whenever is true, is also true
• "Provable"
  • means there exists a proof from the premise to the conclusion
• Soundness
  • Anything that you prove is right
• Completeness
  • You can prove anything that's right

Try not to get too caught-up in your present understanding of proofs and logic. Note that similar to how you went from geometric vectors to abstract vectors, you will have to discard some previous biases/knowledge of logic. What we are doing in formal proofs is a lot more like programming, where proofs have strict syntax that needs formal specification.

Also note that each type of logic is its own "world" or "programming language" (or "space" in mathematics).

Any logic has three parts to it:

1. Syntax
   • Symbols to encode logic
2. Semantics
   • Meanings of symbols
3. Proof theories (aka deductive systems)
   • Proving statements

The syntax of a logic defines how to arrange symbols into a well-formed formula (wff)

""" (entails) for a logic describes what it means for an argument to be "true" in that logic

For a WFF , depending on the context, we call :

• an argument
• a valid argument (if it has been determined to be valid)
• a goal (if it is something we want to prove to be valid)
• entails
• logically/semantically implies

• : from the premises , we may conclude
  • I.e there is no valuation which makes true and the conclusion false
• : whenever is true, is true
• : is always true (a theorem, valid)

A proof theory defines "" (proves)

means using , we can prove using a proof theory.

That is, in some relevant deductive system, there exists a proof from the premises to the conclusion .

• If , we can conclude that
• If , we can conclude that

• Soundness:
  • you can only prove valid arguments
  • if you prove something, it's right
  • if something is wrong, you can't prove it
• Completeness:
  • you can prove all valid arguments
  • if you can't prove something, it's wrong
  • if something is right, you can prove it

A proof theory is sound whenever , then

Soundness states that

That is, if you can prove from , then is true given . The contrapositive of this is if is false given , then you cannot prove from .
In other words, you can't prove something that's wrong, and if you prove something, it's right.

A proof theory is complete whenever , then

Completeness states that

That is, if is true given , then you can prove from . The contrapositive of this is if you cannot prove from , then is false given .
In other words, you can prove anything that's right, and if you can't prove something, it's wrong.

A paradox is a valid argument leading to a contradiction

If the barber of Seville is a man in Seville who shaves all men in Seville who don't shave themselves, and only those men, what man in seville shaves the barber?

Answering this question results in a contradiction.

The barber cannot shave himself since he only shaves those who do not shave themselves. As such, if he shaves himself, he ceases to be the barber.

Conversely, if the barber does not shave himself, then he fits into the group of people who would be shaved by the barber, and thus, as the barber, he must shave himself.

A decision problem is a subset of problems, which have yes or no answers

Unsolvable (undecidable) problems are decision problems for which no algorithm can exist to solve it

• Propositional logic is decidable. For any argument, in propositional logic, there exist an algorithm/computer program to determine if it is valid or not
• Predicate logic is undecidable. There cannot exist an algorithm that will always determine if an argument in predicate logic is valid or not.
  • Subsets of predicate logic are decidable, SMT solvers can determine the validity of many arguments (but not all)
  • Predicate logic is semi-decidable