Judgements and Propositions

We state “A is true”, then “A” is a proposition, and “A is true” as a whole is a judgement.

Some examples of application of logic branches in programming languagues:

Defining a JudgementPermalink

To define a judgement, we must have Introduction rules ($I$), and Elimination rules ($E$). They must satisfy Local Soundness (checks elimination rules are not too strong) such that for every way to apply the elimination rules, we can reduce it to one that already existed. The process of doing that is called local reduction. ($\beta$ rule) They should also satisfy Local Completeness (checks elimination rules are not too weak) such that there is someway to apply the elimination rules so that from the pieces we can re-introduce what the original proposition is. The process of doing that is called local expansion. ($\eta$ rule)

Note: $MN$ means $M$ applies to $N$

Some notations:

$\Gamma ⊢M:A$ means $M$ is a proof of $A$ is $true$, or $M$ is a program of type $A$, where $\Gamma :=\cdot |{\Gamma }^{\prime }x:A$

$\left[N/x\right]M$ means substitude $N$ for $x$ based on the structure of $M$ (plug in $N$ for $x$)

ExamplesPermalink

To define $A\wedge Btrue$:Permalink

Introduction rule ($I$):

or

Elimination rules ($E$):

or

or

Check Local Soundness by local reduction:

or

or

Check Local Completeness by local expansion:

or

To define implication($\supset$):Permalink

Introduction rule($I^x$) (x means an assumption):

or

Elimination rule($E$):

or

Local reduction:

Local expansion: