Наборные логические доказательства в ЛАТЕКСЕ
Я пытаюсь набрать некоторые доказательства основной логики в ЛАТЕКСЕ. Мне нужны несколько расположение столбца, и мне нужны строки, пронумерованные справа. Я хочу сбросить нумерацию для каждого доказательства. Вывод должен быть похожим на это:
1) (x)¬F A
2) (Ex)F
3) ...
Что самый легкий путь состоит в том, чтобы сделать это? перечислите не кажется хорошей идеей, так как она не собирается любить несколько вещей столбца. Мне нужно все, чтобы быть в mathmode также.
Существует ли простой способ сделать это?
[редактирование] Здесь - то, что мне удалось сделать до сих пор, но это совсем не изящно.
\begin{minipage}{\linewidth}
\boldmath \center{$ \forall x \neg F \to \neg \exists x F $} \unboldmath
\begin{math}
\begin{array}{llr}
1. &\forall x \neg F & \\
2. &\exists x F & A \\
3. &F[\alpha / x ] & ES 2 \\
4. &\neg F[\alpha / x] & US \\
5. &\exists x F \to F[\alpha / x ] & CP 2,4 \\
6. &\neg \exists x F & TI 4,5
\end{array}
\end{math}
\end{minipage}
Идеально я хочу что-то, что автоматически числа ступают и делают строку "заголовка" легче...
4 ответа
См. Пакеты доказательств в стиле Fitch здесь . Никаких дополнительных доказательств вам просто не нужно. LaTeX для логиков также охватывает другие стили доказательства, логические символы и т. Д.
\newcount\mycount
\def\nextnum{\global\advance\mycount 1 \the\mycount.}
\def\logicx#1{\halign{$\nextnum##$\quad \hfil&$##$\hfil
&\qquad\hfil##\crcr#1\crcr}\endgroup}
\def\logic{\begingroup \global\mycount 0 \let\\\cr \logicx}
\logic{
&\forall x \neg F & \\
&\exists x F & A \\
&F[\alpha / x ] & ES 2 \\
&\neg F[\alpha / x] & US \\
&\exists x F \to F[\alpha / x ] & CP 2,4 \\
&\neg \exists x F & TI 4,5 \\
}
Извините, у меня сейчас нет компилятора \ LaTeX, поэтому мой код может не компилироваться или содержать глупые ошибки.
Вам нужен новый счетчик для ваших строк:
\newcount\logicproofline
Затем вам понадобится команда для его запуска:
\def\proofline#1{
\global\advance\logicproofline by 1
\shoveright{\text{\the\logicproofline}\qquad#1}
}
Теперь вам нужно переопределить proof , чтобы сбросить счетчик:
\AtBeginDocument{
\let\myoldproof=\proof
\def\proof{\myoldproof\logicproofline=0\relax}
}
Переопределение необходимо, потому что доказательство не связано ни с одним счетчиком, поэтому мы не можем сделать его главным счетчиком.