<commit_before>#+Title: Logic and Proof
#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]], [[http://https://www.andrew.cmu.edu/user/rlewis1/][<NAME>]],  [[http://http://www.contrib.andrew.cmu.edu/~fpv/][<NAME>]]

* Truth Tables and Semantics

In the last chapter, we saw how to prove a formula of propositional
logic from hypotheses. Some formulas are provable outright, from no
hypotheses at all, such as the formula $A \to A$.

It seems intuitively clear that, in contrast, we cannot prove the
formula $A \to B$ without additional assumptions. Try it in Lean:
#+BEGIN_SRC lean
variables A B : Prop

example : A → B :=
assume H : A,
show B, from sorry
#+END_SRC
It should seem unlikely that there is an argument we could put in
place of the "sorry" to complete this proof. After all, =B= could be
false!

What do we mean by "false," exactly? We used the identifiers =true=
and =false= to denote certain propositions in Lean, but here we are
using the words in a difference sense, as values, or judgments, we
can assign to propositional formulas. Such evaluations belong to the
realm of /semantics/. Formulas and formal proofs are /syntactic/
notions, which is to say, they are represented by symbols and symbolic
structures. Truth is a /semantic/ notion, in that it ascribes a type
of /meaning/ to certain formulas.<commit_msg>fix(03): add ID to chapter title, for reference from Chapter 7<commit_after>#+Title: Logic and Proof
#+Author: [[http://www.andrew.cmu.edu/user/avigad][<NAME>]], [[http://https://www.andrew.cmu.edu/user/rlewis1/][<NAME>]],  [[http://http://www.contrib.andrew.cmu.edu/~fpv/][Fl<NAME>]]

* Truth Tables and Semantics
:PROPERTIES:
  :CUSTOM_ID: Truth_Tables_and_Semantics
:END:

In the last chapter, we saw how to prove a formula of propositional
logic from hypotheses. Some formulas are provable outright, from no
hypotheses at all, such as the formula $A \to A$.

It seems intuitively clear that, in contrast, we cannot prove the
formula $A \to B$ without additional assumptions. Try it in Lean:
#+BEGIN_SRC lean
variables A B : Prop

example : A → B :=
assume H : A,
show B, from sorry
#+END_SRC
It should seem unlikely that there is an argument we could put in
place of the "sorry" to complete this proof. After all, =B= could be
false!

What do we mean by "false," exactly? We used the identifiers =true=
and =false= to denote certain propositions in Lean, but here we are
using the words in a difference sense, as values, or judgments, we
can assign to propositional formulas. Such evaluations belong to the
realm of /semantics/. Formulas and formal proofs are /syntactic/
notions, which is to say, they are represented by symbols and symbolic
structures. Truth is a /semantic/ notion, in that it ascribes a type
of /meaning/ to certain formulas.
{'fraction_non_alphanumeric': 0.0968783638320775, 'fraction_numerical': 0.001794043774668102, 'mean_word_length': 4.371868978805395, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 2, 'lorem ipsum': 0, 'www.': 6, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6417219', 'n_tokens_mistral': 876, 'n_tokens_neox': 827, 'n_words': 407}