Quick Overview:
   - I just taught first year logic for the first time
      and I have gotten very positive feed back from the students so far.
   - I received a lot of insights from Toniann Pitassi and Russell Impagliazzo.
   - For better or worse, I don't follow a book.
   - Working crazy crazy hard, I made about 1500 slides and lots of videos.
   - I would LOVE your feed back and for someone to use my slides and videos.
      https://www.eecs.yorku.ca/~jeff/courses/1090/syllabus/
      https://www.eecs.yorku.ca/~jeff/courses/1090/syllabus/thoughts.html
   - I have never liked the way logic was taught
      because I found it very formal, mechanical, and void of meaning.
      I find that students entering upper year courses, fail to understand the basics of logic.
   - The key for me is the difference between
        - ∃Machine M, ∀Input I, P(I)=M(I) (ie problem P is computable)
        - ∀Input I, ∃Machine M, P(I)=M(I) (Aaaaah)
   - As such I focused more on meaning, two proof systems I "invented",
      and computer science examples.
          - Game: I define a game with an oracle, prover, and adversary
             that informally proves a sentence is valid by following its parsing.
             To prove A → ∀x ∃y α(x,y,z)
                 - the adversary provides an arbitrary model, function for α, and value for z,
                 - the oracle assures you of A,
                 - the adversary provides an arbitrary value for x,
                 - and the prover provides a corresponding value for y that works.
          - Skolem/Auxiliary: Another way is to understand ∀x ∃y α(x,y,z) is
                 - ∀α,z, ∃function y, ∀x α(x,y(x),z)
          - Formal Proof System: I make small changes to the more standard formal proof system
                 - so it is not a "proof" that there is a proof
                 - to be more intuitive
                 - so that soundness follows easily from understanding the meaning of each line.
          - Davis Putnam: I define a new proof system for proving propositional tautologies
             that mirrors a Davis Putnam Computation.
          - Computer Science Examples: I made more slides than I was able to get to,
             to cover most undergrad topics in computer science theory.
                 - Computable vs Uncomputable, Deterministic vs Probabilistic Algorithms,
                 - Time Complexity, Compile Time vs Run Time, Big-Oh Notation,
                 - Compiling a Java program into a TM, Universal TM,
                 - Computing vs Accepting, Poly vs NP, Reductions, Uncomputable Problems
                 - Graphs, Finite Fields, Vector Spaces, Information Theory
   - Again I would LOVE your feed back!

Understanding:
   - Jeff feels VERY strongly that the students need to feel physical pain
      when they see incorrect statements like "∀Inputs I, ∃Java program J, J(I)=P(I)".
       All the way through grad school they don't get this. How can they do any math without it?
   - We will cover lots of intuition for lots of practical examples
       that are crucial for understanding Computer Science.
   - And we will balance understanding, informal intuitive and formal mechanical proofs.

How to Think About Proof Systems:
   - Jeff's goal is to get the students to be as passionate about the material as he is.
   - He wants to teach them, not just what to think, but how to think.
   - This means that he tends to make up new things to teach.
   - Every term some students and professors complain that this makes it harder for them.
   - But many really like it.

Non-Standard:
   - Jeff tries to explain, but he upsets some professors.
       They say "The Rules taught should be the ones our forefathers devised. All else is dangerous".
   - Adding meaning (semantics) or intuition is also bad.
   - Jeff found our forefathers' formal proof system overly complicated and lacking (at least his) intuition.

Its a Game:
   - George firmly states that he does not play games.
   - For 25 years, in every course, Jeff covers an informal Game as a proof system for first order logic.
   - Reading left to right, the prover provides for ∃x & the adversary provides for ∀y.
       The key is that the order in which the players go is crucial to who wins.
          - Lets each choose a number and the one with the biggest number wins. You go first.
   - The formula is proofed to be valid by giving a winning strategy for the corresponding game.
   - For example, with "∀Inputs I, ∃Java program J, J(I)=P(I)":
          - The adversary tells me his worst input I.
       - Knowing his I and P(I), the prover writes the one line of code J that outputs the answer P(I).
          - Even worse, even if the prover is unable to compute P(I) from I,
      he still knows that it has some well defined answer
      and hence the Java program outputting it does exist, i.e. ∃J.

Local Rules and Meaning:
   - Our forefathers teach meta rules which say how to symbolically
       translate a proof with one syntax into a Hilbert style proof, i.e. one in which:
       - One line follows mechanically from previous lines.
       - But is too hard to follow directly even for the expert
   - I find this more confusing then necessary, lacking the locality required for a Hilbert style proof,
          and not in line with my intuition.
   - Problem 1: x vs x'
       - Standard deduction is to assume α(x), prove β(x) and conclude α(x)→β(x).
       - The challenge is that while you are assuming the "hypothesis" α(x), you need to treat x not as a free variable, but as a fixed constant.
       - Different rules can be applied to this variable x.
       - This lacks locality because which rules you are allowed to apply to a given line
          requires looking earlier in the proof to see the status of its variables.
       - To solve this problem, Jeff introduces new notation x' to locally remind people of the status of this variable.
   - Problem 2: x vs x_∃
       - One of the meta rules says that after line ∀x α(x) in your proof, one can put the line α(r).
       - Another says that if you have proved ∃ x α(x), then you can remove the exists and continue a "separate" proof from α(r).
          In practice, this seems to be written as having line α(r) appear after line ∃x α(x) in what looks like a proof.
       - What is confusing to Jeff is having the same line α(r) appearing twice with completely different meanings.
       - It is true that these two proofs allow different next steps based on which meta rule you are applying,
          but as said this means that it lacks the locality of a Hilbert proof.
       - Jeff's solution to this problem is to use the notation α(x_∃) when coming from line ∃x α(x).
       - This notation x_∃ locally flags the required global information making the rules
          seem even more symbolically mechanical and Hilbert like.
       - The notation also emphasizes the semantic meaning of each line. (Against our forefathers' wishes)
          The line α(x) now has the implied meaning ∀x α(x) and the line α(x_∃) the meaning ∃x α(x).
       - It gives the proof its sound semantics.
       - We call this implied longer meaning/syntax the "Quantifier Closure".
          It is a generalization of the standard concept of a Universal Closure.
       - Jeff feels the students should not just be a mechanical automita, but need to understand this meaning.
   - For Instructors and Experts: See (ppt) for a quick comparison of our forefathers' proof systems and ours.

Propositional Proof System from the Recursive Search Algorithm:
   - Some sections of 1090 spend much of the term teaching a complicated formal proof system
       for proving propositional formulas are tautologies
       (i.e. whether a given And/Or/Not formula evaluates to be true under every true/false assignment.)
   - Jeff feels that theoretically, a 2ⁿ sized truth table serves as an easier to understand proof.
       And according to NP vs Co-NP theory there are not smaller proofs in general.
   - Gödel, himself, had a nice parallel between Proofs and Computation. Lets elaborate on this.
   - Sometimes a truth table search can be shortened using a simple Recursive-Backtracking Davis-Putnam algorithm
       for finding a good True/False assignment for a propositional formula.
   - Because this course is to teach formal proof systems for computer science,
       Jeff writes down a few obvious rules.
       - These rules produce a proof that mirrors this Davis Putnam computation.
       - Because we know that Davis Putnam can handle any instance,
           this mirroring ensures that this new proof system is Complete,
           i.e. it can prove all propositional tautologies.
          - Because each rule follows from a tautology (with a small truth table),
           we also know that the proof system is also Sound.
       - Because it has a constant size proof of each of the rules of the other proof systems,
           its smallest proof for a given formula can't be much bigger or complicated than theirs.

Propositional Proof System from Standard Proof Techniques:
   - The proof techniques that need to be covered are:
       Deduction, Proof by Cases, Modus Ponens,
       Contrapositive (Correlation of → does imply Causality),
       Using easy Tautologies (De Morgan's Law, Distributive, Communicative)
       Transitivity, Proof by Contradiction, and Concluding anything from A and ¬A.
   - So that this is not just magical, Jeff makes each of these into a simple propositional tautology formula.
   - Jeff then makes each into a formal proof system rule
          so that the formal proof system follows the intuitive proofs that people actually use in practice.

Short and Elegant vs Useful:
   - Because it is fun to have a really trimmed down proof system from which you can prove everything,
       one with a short list of rules is covered.
   - Because it is also fun to have a really intuitive and robust proof system from which proving things is easy,
       one with an additional list of rules is also covered.
   - All of these fore mentioned rules are then neatly subsumed by the one basic rule
           (and in the darkness bind them)
       that allows one to make a lemma out of any previously proved tautology.

All Made Up:
   - One could say that Jeff just "made up" these proof systems, but that would be too generous to him.
   - Please indulge him.
   - He does believe that they are easier to understand.
   - And do not veer too far from what our forefathers did.
   - He hopes that they are better for first year students.
   - Warning: Jeff has never taught 1090 before.

Cover ALL of Computer Science Theory:
   - Generalizing: One point of formal proofs is to prove theorems with as few assumptions as possible about the nature
       of the objects in our Universe so that we can find a wide range of strange new objects for which the same theorems are true.
   - We intend to cover the first order logic needed to be able to express all the concepts covered in 2001, 3101, 6111,...
       Computable vs Uncomputable, Deterministic vs Probabilistic Algorithms,
       Time Complexity, Compile Time vs Run Time, Big-Oh Notation,
       Compiling a Java program into a TM, Universal TM,
       Computing vs Accepting, Poly vs NP, Reductions, Uncomputable Problems
       Graphs, Finite Fields, Vector Spaces, Information Theory
   - You must be saying "too hard"!!! But our goal is much more humble.
       We want first year students to be able to read and understand
       the key first order logic statements that arise from these topics.
   - Examples:
         - Classifying Functions: ∃c∃n₀∀n≥n₀ f(n) ≤ cg(n)
             We can certainly prove this for example f&g using our proof system.
         - Uncomputable Problems: ∃P∀M∃I M(I)≠P(I)
             Without a doubt, we want the students to learn that this means that there are uncomputable problems.
             It may to ambitions, but the formal proof of this fits on a quarter page.
         - Gödel's Incompleteness Theorem: Could the students handle a 20 min explanation.
             If there was a sound and complete proof system,
             then it would be decidable whether a given first order logic sentence was valid.
             and then it would be decidable whether a given TM halted. But this is not the case.
         - Compiling: ∀ Java Programs J, ∃ TM M, ∀ input I, J(I)=M(I)
             We would say that TM is a theoretical model of computation. (Flash a picture of one.)
             The students would need to know that a proof of this involves
             compiling a given Java program into an equivalent TM. (Zero details. Maybe flash a picture.)
         - Graphs: Out degree one ≡ ∀u∃v[Edge(u,v) & ∀v'≠v ¬Edge(u,v')]
             If you can only talk about nodes and edges, then you can't say that the graph is connected or that it is finite.
             Similarly, you can't say whether the your field contains an infinite number of integers.
             This is partly why we have non-standard models.
             On the other hand, if you can talk about finite paths, then you define whether the graph is connected,
             i.e. ∀u,v ∃ path P(u,v).
         - Vector Spaces: ∀V, ∀⟨w₁...w_d⟩, ∀v∈V, ∃⟨c₁...c_d⟩, v=c₁w₁+...+c_dw_d
             Suppose they were promised that this was true.
             We would define a Vector Space V to be an arbitrary set of objects for which v=c₁w₁+...+c_dw_d is well defined.
             They then could define their own Vector Space V and two different bases ⟨w₁...w_d⟩ and ⟨w'₁...w'_d⟩.
             And be ensured to have black box oracle for translating a vector of coefficients ⟨c₁...c_d⟩
             with respect to the first basis into a vector of coefficients ⟨c'₁...c'_d⟩ with respect to the second.
             We would then devote 2 min per application, eg Error Correcting Codes, Fourier Transformations, JPEG,
             Integer Multiplication, Dimension Reduction, & Differentiation of Functions.
   - If it becomes too much, we will cut things out as we go.
   - We think it would be good for the students to have this early introduction.