|
This video includes a couple of points from a 2019 review lecture on Sequents.First we discuss how to use reduction to find an inhabited model in which Γ ⊨ Δ, which is equivalent to…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
Gentzen's rules provide a complete system that does not require the cut rule. For many logical systems, cut elimination (showing that uses of the cut rule may be eliminated from any sound proof)…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
We introduce sequents, where we have finite sets of predicates on both sides of the turnstile.
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|
|
In week 4 we introduced Gentzen's sequents.You should make sure you understand when a sequent is valid, and what it means to provide a counter-example to a sequent -- a universe in which the…
Course Code
INFR08025 Licence Type
All rights reserved The University of Edinburgh Language
English
|