Skip to content

Commit

Permalink
Spell check and topological semantics fixups (#355)
Browse files Browse the repository at this point in the history
* index.start.html: Spell check

* topological-semantics.tex: Replace period with question mark

* topological-semantics.tex: Split up long paragraph

* topological-semantics.tex: Expand terse sentences

* topological-semantics.tex: Split out tricky paragraph

Technically this paragraph answers part of the question that starts the
previous paragraph, but readers should be able to follow.
  • Loading branch information
davidvandebunte authored Jan 24, 2024
1 parent d541bf0 commit 0f03675
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 19 deletions.
39 changes: 21 additions & 18 deletions content/intuitionistic-logic/semantics/topological-semantics.tex
Original file line number Diff line number Diff line change
Expand Up @@ -69,24 +69,27 @@
only the !!{element}s of $\Top{O}$ are. $!A \Entails !B$ iff $!B$ is
true at every point at which~$!A$ is true, i.e., $\Prop{X}{!A}
\subseteq \Prop{X}{!B}$, for all~$X$. The absurd statement~$\lfalse$
is never true, so $\Prop{X}{\lfalse} = \emptyset$. How must the
propositions expressed by $!B \land !C$, $!B \lor !C$, and $!B \lif
!C$ be related to those expressed by $!B$ and~$!C$ for the
intuitionistically valid laws to hold, i.e., so that $!A \Proves !B$
iff $\Prop{X}{!A} \subset \Prop{X}{!B}$. $\lfalse \Proves !A$ for any
$!A$, and only $\emptyset \subseteq U$ for all $U$. Since $!B \land
!C \Proves !B$, $\Prop{X}{!B \land !C} \subseteq \Prop{X}{!B}$, and
similarly $\Prop{X}{!B \land !C} \subseteq \Prop{X}{!C}$. The largest
set satisfying $W \subseteq U$ and $W \subseteq V$ is $U \cap V$.
is never true, so $\Prop{X}{\lfalse} = \emptyset$.

How must the propositions expressed by $!B \land !C$, $!B \lor !C$,
and $!B \lif !C$ be related to those expressed by $!B$ and~$!C$ for
the intuitionistically valid laws to hold, i.e., so that $!A \Proves
!B$ iff $\Prop{X}{!A} \subset \Prop{X}{!B}$? We require $\lfalse
\Proves !A$ for any $!A$, which is satisfied because $\emptyset
\subseteq U$ for all $U$. Since $!B \land !C \Proves !B$, we require
that $\Prop{X}{!B \land !C} \subseteq \Prop{X}{!B}$, and similarly
$\Prop{X}{!B \land !C} \subseteq \Prop{X}{!C}$. The largest set
satisfying $W \subseteq U$ and $W \subseteq V$ is $U \cap V$.
Conversely, $!B \Proves !B \lor !C$ and $!C \Proves !B \lor !C$, and
so $\Prop{X}{!B} \subseteq \Prop{X}{!B \lor !C}$ and $\Prop{X}{!C}
\subseteq \Prop{X}{!B \lor !C}$. The smallest set~$W$ such that $U
\subseteq W$ and $V \subseteq W$ is $U \cup V$. The definition for
$\lif$ is tricky: $!A \lif !B$ expresses the weakest proposition that,
combined with $!A$, entails $!B$. That $!A \lif !B$ combined with $!A$
entails~$!B$ is clear from $(!A \lif !B) \land !A \Proves !B $. So
$\Prop{X}{!A \lif !B}$ should be the greatest open set such that
$\Prop{X}{!A \lif !B} \cap \Prop{X}{!A} \subset \Prop{X}{!B}$, leading
to our definition.
so we require that $\Prop{X}{!B} \subseteq \Prop{X}{!B \lor !C}$ and
$\Prop{X}{!C} \subseteq \Prop{X}{!B \lor !C}$. The smallest set~$W$
such that $U \subseteq W$ and $V \subseteq W$ is $U \cup V$.

The definition for $\lif$ is tricky: $!A \lif !B$ expresses the
weakest proposition that, combined with $!A$, entails $!B$. That $!A
\lif !B$ combined with $!A$ entails~$!B$ is clear from $(!A \lif !B)
\land !A \Proves !B $. So $\Prop{X}{!A \lif !B}$ should be the
greatest open set such that $\Prop{X}{!A \lif !B} \cap \Prop{X}{!A}
\subset \Prop{X}{!B}$, leading to our definition.

\end{document}
2 changes: 1 addition & 1 deletion misc/index.start.html
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ <h3><a href="https://ic.openlogicproject.org/"><em>Incompleteness and Computabil
<h3><a href="https://bd.openlogicproject.org/"><em>Boxes and Diamonds</em></a></h3>

<p><a href="https://bd.openlogicproject.org/"><img src="https://bd.openlogicproject.org/bd.png" /></a>A textbook for modal and other intensional logics based on the Open Logic Project; includes the material on normal modal logic,
intutionistic logic, and counterfactuals, with appendices on basic
intuitionistic logic, and counterfactuals, with appendices on basic
set theory and classical propositional logic.</p>

<ul>
Expand Down

0 comments on commit 0f03675

Please sign in to comment.