The {{c1::set of statements \(\mathcal{S}\)}} is denoted as a subset of the finite bit strings \(\Sigma^*\).
Note 1: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
BTm~S%al=(
Previous
Note did not exist
New Note
Front
Back
The {{c1::set of statements \(\mathcal{S}\)}} is denoted as a subset of the finite bit strings \(\Sigma^*\).
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | The {{c1::set of statements \(\mathcal{S}\)}} is denoted as {{c2:: a subset of the finite bit strings \(\Sigma^*\)}}. |
Note 2: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
nNq&rzbEm:
Previous
Note did not exist
New Note
Front
Every statement \(s \in \mathcal{S}\) is either true or false as assigned by the {{c2:: truth function \(\tau : \mathcal{S} \rightarrow \{0,1\}\) which assigns to each statement it's truth value}}.
Back
Every statement \(s \in \mathcal{S}\) is either true or false as assigned by the {{c2:: truth function \(\tau : \mathcal{S} \rightarrow \{0,1\}\) which assigns to each statement it's truth value}}.
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | Every statement \(s \in \mathcal{S}\) is {{c1:: either true or false}} as assigned by the {{c2:: truth function \(\tau : \mathcal{S} \rightarrow \{0,1\}\) which assigns to each statement it's <b>truth value</b>}}. |
Note 3: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
clQ8TG-]Z`
Previous
Note did not exist
New Note
Front
The truth function \(\tau : \mathcal{S} \rightarrow \{0,1\}\) defines the meaning or semantics in \(\mathcal{S}\).
Back
The truth function \(\tau : \mathcal{S} \rightarrow \{0,1\}\) defines the meaning or semantics in \(\mathcal{S}\).
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | The truth function \(\tau : \mathcal{S} \rightarrow \{0,1\}\) defines the {{c1:: meaning or <i>semantics</i>}} in \(\mathcal{S}\). |
Note 4: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
b$)[z:.0@q
Previous
Note did not exist
New Note
Front
{{c2::\(\mathcal{P} \subseteq \Sigma^*\)}} is the set of (syntactic representations of) proof strings.
Back
{{c2::\(\mathcal{P} \subseteq \Sigma^*\)}} is the set of (syntactic representations of) proof strings.
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | {{c2::\(\mathcal{P} \subseteq \Sigma^*\)}} is the set of {{c1:: (syntactic representations of) proof strings}}. |
Note 5: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
ui6=/w5,Pi
Previous
Note did not exist
New Note
Front
An element \(p \in \mathcal{P}\) is either a valid proof for a statement \(s \in \mathcal{S}\) or it's not. this is defined by the {{c1:: verification function \(\phi : \mathcal{S} \times \mathcal{P} \rightarrow \{0, 1\}\) }}.
Back
An element \(p \in \mathcal{P}\) is either a valid proof for a statement \(s \in \mathcal{S}\) or it's not. this is defined by the {{c1:: verification function \(\phi : \mathcal{S} \times \mathcal{P} \rightarrow \{0, 1\}\) }}.
\(\phi(s, p) = 1\) means that \(p\) is a valid proof for \(s\).
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | An element \(p \in \mathcal{P}\) is either a valid proof for a statement \(s \in \mathcal{S}\) or it's not. this is defined by the {{c1:: <b>verification function</b> \(\phi : \mathcal{S} \times \mathcal{P} \rightarrow \{0, 1\}\) }}. | |
| Extra | \(\phi(s, p) = 1\) means that \(p\) is a valid proof for \(s\). |
Note 6: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
E,Vbly-9X8
Previous
Note did not exist
New Note
Front
A proof system \(\Pi\) is {{c1:: a quadruple \(\Pi = (\mathcal{S, P}, \tau, \phi)\)}}.
Back
A proof system \(\Pi\) is {{c1:: a quadruple \(\Pi = (\mathcal{S, P}, \tau, \phi)\)}}.
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | A proof system \(\Pi\) is {{c1:: a quadruple \(\Pi = (\mathcal{S, P}, \tau, \phi)\)}}. |
Note 7: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
BYs?C)>Q^q
Previous
Note did not exist
New Note
Front
A proof system is sound if no false statement has a proof: \(\phi(s, p) = 1 \implies \tau(s) = 1\).
Back
A proof system is sound if no false statement has a proof: \(\phi(s, p) = 1 \implies \tau(s) = 1\).
Note that the use of \(\implies\)is not the correct formalism.
For all \(s \in \mathcal{S}\) for which there exists a \(p \in \mathcal{P}\) with \(\phi(s, p) = 1\), we have \(\tau(s) = 1\) is the correct formal definition.
For all \(s \in \mathcal{S}\) for which there exists a \(p \in \mathcal{P}\) with \(\phi(s, p) = 1\), we have \(\tau(s) = 1\) is the correct formal definition.
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | A proof system is {{c2:: <b>sound</b>}} if {{c1:: no false statement has a proof: \(\phi(s, p) = 1 \implies \tau(s) = 1\)}}. | |
| Extra | <i>Note that the use of </i>\(\implies\)<i>is not the correct formalism.<br></i><br>For all \(s \in \mathcal{S}\) for which there exists a \(p \in \mathcal{P}\) with \(\phi(s, p) = 1\), we have \(\tau(s) = 1\) is the correct formal definition. |
Note 8: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
fDaa%yb|#1
Previous
Note did not exist
New Note
Front
A proof system is complete if every true statement has a proof: \(\phi(s, p) = 1 \Longleftarrow \tau(s) = 1\).
Back
A proof system is complete if every true statement has a proof: \(\phi(s, p) = 1 \Longleftarrow \tau(s) = 1\).
Note that the use of \(\Longleftarrow\) is not the correct formalism.
For all \(s \in \mathcal{S}\) with \(\tau(s) = 1\) there exists a \(p \in \mathcal{P}\) such that \(\phi(s, p) = 1\), is the correct formal definition.
For all \(s \in \mathcal{S}\) with \(\tau(s) = 1\) there exists a \(p \in \mathcal{P}\) such that \(\phi(s, p) = 1\), is the correct formal definition.
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | A proof system is {{c2:: <b>complete</b>}} if {{c1:: every true statement has a proof: \(\phi(s, p) = 1 \Longleftarrow \tau(s) = 1\)}}. | |
| Extra | <i>Note that the use of </i> \(\Longleftarrow\) <i>is not the correct formalism.</i><br>For all \(s \in \mathcal{S}\) with \(\tau(s) = 1\) there exists a \(p \in \mathcal{P}\) such that \(\phi(s, p) = 1\), is the correct formal definition. |
Note 9: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
Llw?`Jb)R)
Previous
Note did not exist
New Note
Front
We require that the proof verification function \(\phi\) is efficiently computable, otherwise the proof system is not useful.
Back
We require that the proof verification function \(\phi\) is efficiently computable, otherwise the proof system is not useful.
A proof system is useless if verification is infeasible.
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | We require that the proof verification function \(\phi\) is {{c1::efficiently computable}}, otherwise the proof system is not useful. | |
| Extra | A proof system is useless if verification is infeasible. |
Note 10: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
qFYoZgCSMu
Previous
Note did not exist
New Note
Front
The predicate \(\tau\) defines the {{c1:: set of strings \(L \subseteq \{0, 1\}\) that correspond to true statements}}.
Back
The predicate \(\tau\) defines the {{c1:: set of strings \(L \subseteq \{0, 1\}\) that correspond to true statements}}.
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | The predicate \(\tau\) defines the {{c1:: set of strings \(L \subseteq \{0, 1\}\) that correspond to true statements}}. |
Note 11: ETH::DiskMat
Deck: ETH::DiskMat
Note Type: Horvath Cloze
GUID:
added
Note Type: Horvath Cloze
GUID:
K5psNfU-&?
Previous
Note did not exist
New Note
Front
\( L = \{s \ | \ \tau(s) = 1\} \) is a set of strings called a formal language. It defines a predicate \(\tau\).
Back
\( L = \{s \ | \ \tau(s) = 1\} \) is a set of strings called a formal language. It defines a predicate \(\tau\).
Field-by-field Comparison
| Field | Before | After |
|---|---|---|
| Text | \( L = \{s \ | \ \tau(s) = 1\} \) is a set of strings called a {{c1:: formal language}}. It defines a {{c2:: predicate \(\tau\)}}. |