On 12/25/25 10:07 AM, Stefano Simonucci wrote:
I have not been able to get pythontex to work. Has anyone else done
this? Do you have any examples?
This is not in LyX, but is the one application I've made of the python
package. It does have some other dependencies, but of course you can
install those.
Riki
On 12/23/25 17:01, Neal Becker wrote:
Has anyone used pythontex and can it be used with LyX?
Thanks,
Neal
--
/Those who don't understand recursion are doomed to repeat it/
--
----------------------------
Richard Kimberly (Riki) Heck
Professor of Philosophy and Professor of Linguistics
Brown University
Pronouns: they/them/their
Website:http://rkheck.frege.org/
\documentclass[letterpaper,11pt]{paper}
\usepackage[utf8]{inputenc}
\usepackage{newcent}
\usepackage{helvet}
\usepackage{courier}
\usepackage{natded}
\usepackage{python}
\date{}
\usepackage{amsmath,amssymb}
\usepackage{amsthm}
\makeatletter
\theoremstyle{definition}
\newtheorem{xca}{Exercise}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\newcounter{lastthm}
\newcounter{tempthm}
\setcounter{lastthm}{0}
\newcommand\resetthm{
\clearpage
\setcounter{tempthm}{\value{lastthm}}
\setcounter{lastthm}{\value{xca}}
\setcounter{xca}{\value{tempthm}}
}
\newcommand\makeex[2]{%
\expandafter\newcommand\csname EX#1\endcsname{\begin{xca}#2\end{xca}}%
\csname EX#1\endcsname}
%opening
\title{Problem Set 8:\\Practice Problems}
\begin{document}
\maketitle
\section*{Problems}
\makeex{z}{Show by deduction that $\forall x(Fx \to Gx)$ and $\forall x(\neg Gx)$ imply $\forall x(\neg Fx)$.}
\makeex{a}{Show by deduction that $\forall x(Fx \to Gx)$ and $\forall x(Gx \to Hx)$ imply $\forall x(Fx \to Gx \wedge Hx)$.}
\makeex{b}{Show by deduction that $\exists x\forall y(Rxy)$ implies $\forall y\exists x(Rxy)$.}
\makeex{c}{Show by deduction that $\forall x(Fx\to Gx)$ implies $\forall x[\exists y(Fy\wedge Hxy)\to\exists y(Gy\wedge Hxy)]$.}
\makeex{d}{Show by deduction that $\exists x(Fx\wedge\forall y(Fy\to Gxy))$ implies $\exists x(Gxx)$.}
\resetthm
\section*{Solutions}
\EXz
\begin{python}
from pytest import *
p = Proof()
p.addline("1", "\\forall x(Fx \\to Gx)", "P")
p.addline("2", "\\forall x(\\neg Gx)", "P")
p.addline("1", "Fu \\to Gu", "UI(1)")
p.addline("2", "\\neg Gu", "UI(2)")
p.addline("1,2", "\\neg Fu", "TF(3,4)")
p.addline("1,2", "\\forall x(\\neg Fx)", "UG(5)")
p.wholeproof()
p.pproof([1,2], [6,
[5.0, "Since our conclusion is universal, we will try to prove an instance of it."],
[-3, "No other instance of (1) can help us."],
[-4, 5.0]])
q = Proof()
q.addline("1", "\\forall x(Fx \\to Gx)", "P")
q.addline("2", "\\forall x(\\neg Gx)", "P")
q.addline("3", "\\neg\\forall x(\\neg Fx)", "P")
q.addline("3", "\\exists x(Fx)", "CQ(3)")
q.addline("3,5", "Fa", "EII(4)a")
q.addline("1", "Fa \\to Ga", "UI(1)")
q.addline("1,3,5", "Ga", "TF(5,6)")
q.addline("2", "\\neg Ga", "UI(2)")
q.addline("1,2,3,5", "p \\wedge \\neg p", "TF(7,8)")
q.addline("1,2,3", "p \\wedge \\neg p", "EIE(9)[5]@")
q.addline("1,2", "\\neg\\forall x(\\neg Fx) \\to p \\wedge \\neg p", "D(10)[3]")
q.addline("1,2", "\\forall x(\\neg Fx)", "TF(11)")
q.wholeproof("Another way to do it is by reductio. As you can see, though, that is quite a bit longer.")
\end{python}
\EXa
\begin{python}
from pytest import *
p = Proof()
p.addline("1", "\\forall x(Fx \\to Gx)", "P")
p.addline("2", "\\forall x(Gx \\to Hx)", "P")
p.addline("3", "Fu", "P")
p.addline("1", "Fu \\to Gu", "UI(1)")
p.addline("1,3", "Gu", "TF(3,4)")
p.addline("2", "Gu \\to Hu", "UI(2)")
p.addline("1,2,3", "Hu", "TF(5,6)")
p.addline("1,2,3", "Gu \\wedge Hu", "TF(5,7)")
p.addline("1,2", "Fu \\to Gu \\wedge Hu", "D(8)[3]")
p.addline("1,2", "\\forall x(Fx \\to Gx \\wedge Hx)", "UG(6)")
p.wholeproof()
p.pproof([1,2], [10, 9, [-3,8,
"Since line (9) is a conditional, we make its antecedent a premise and try to proves its consequent"], [5.0,7.0, "Since line (8) is a conjunction, we try to prove both of its conjuncts."], [-4,5.0], [-6,7.0]])
q = Proof()
q.addline("1", "\\forall x(Fx \\to Gx)", "P")
q.addline("2", "\\forall x(Gx \\to Hx)", "P")
q.addline("1", "Fu \\to Gu", "UI(1)")
q.addline("2", "Gu \\to Hu", "UI(2)")
q.addline("1,2", "Fu \\to Gu \\wedge Hu", "TF(3,4)")
q.addline("1,2", "\\forall x(Fx \\to Gx \\wedge Hx)", "UG(6)")
q.wholeproof("There are always many ways to do these problems. What's above is clearly a much shorter deduction. But the other one is easier to construct, in many ways.")
\end{python}
\EXb
\begin{python}
from pytest import *
q = Proof()
q.addline("1", "\\exists x\\forall y(Rxy)", "P")
q.addline("1,2", "\\forall y(Ray)", "EII(1)a")
q.addline("1,2", "Rau", "UI(2)")
q.addline("1,2", "\\exists x(Rxu)", "EG(3)")
q.addline("1", "\\exists x(Rxu)", "EIE[2](4)")
q.addline("1", "\\forall y\\exists x(Rxy)", "UG(5)")
q.wholeproof()
q.pproof([1], [6,
[-2, "The only thing to do with existential premises is instantiate them, so we do that first."],
[5.0, "Our conclusion is universal, so we try to prove an instance of it."],
[-3, "Lacking anything better to do, we take an instance of the universal we now have. The only free variables in play here are $a$ and $u$, and $Raa$ will not help us."], [-4,5.0]])
\end{python}
\EXc
\begin{python}
from pytest import *
p = Proof()
p.addline("1", "\\forall x(Fx\\to Gx)", "P")
p.addline("2", "\\exists y(Fy\\wedge Huy)", "P")
p.addline("2,3", "Fa \\wedge Hua", "EII(2)a")
p.addline("1", "Fa \\to Ga", "UI(1)")
p.addline("1,2,3", "Ga", "TF(3,4)")
p.addline("1,2,3", "Ga \\wedge Hua", "TF(3,5)")
p.addline("1,2,3", "\\exists y(Gy\\wedge Huy)", "EG(6)")
p.addline("1,2", "\\exists y(Gy\\wedge Huy)", "EIE[3](7)")
p.addline("1", "\\exists y(Fy\\wedge Huy) \\to \\exists y(Gy\\wedge Huy)", "D[2](8)")
p.addline("1", "\\forall x[\\exists y(Fy\\wedge Hxy) \\to \\exists y(Gy\\wedge Hxy)]", "UG(9)")
p.wholeproof()
p.pproof([1], [10,
[9, "Universal conclusion, so try to prove an instance."],
[-2,8.0, "Conditional, so assume the antecedent and try to prove the consequent."],
[-3, "Existential premise: Instantiate it!"],
[-4, "What instance of (1) will help us? Well, we have $Fa$ already\dots"],
-5, -6, [-7,8.0]])
\end{python}
\EXd
\begin{python}
from pytest import *
p = Proof()
p.addline("1", "\\exists x(Fx \\wedge \\forall y(Fy \\to Gxy))", "P")
p.addline("1,2", "Fa \\wedge \\forall y(Fy \\to Gay))", "EII(1)a")
p.addline("1,2", "\\forall y(Fy \\to Gay))", "TF(2)")
p.addline("1,2", "Fa \\to Gaa", "UI(3)")
p.addline("1,2", "Gaa", "TF(2,4)")
p.addline("1,2", "\\exists x(Gxx)", "EG(5)")
p.addline("1", "\\exists x(Gxx)", "EIE(6)[2]")
p.wholeproof()
p.pproof([1], [7.0,
[-2, "Take an instance of the existential, since there's nothing else to do with them."],
[-3, "Remember that you can only use UI on a universal statement! In particular, it would be a mistake to write $Fa \\wedge (Fa \\to Gaa)$ here!"],
[-4, "What instance of (3) will help us here? The only variable that is really in play is $a$, so why not that one?"],
-5,
[-6,7.0]])
\end{python}
\end{document}
#!/usr/bin/python
class ProofLine:
def __init__(self, prems, schema, just):
self.prems = prems
self.schema = schema
self.just = just
def dummy(self):
print("\\makeatletter\\refstepcounter{@NDlines}\\makeatother\dots{}\n")
def pout(self, docite = True):
if docite:
print("\\ndl{%s}{%s}{%s}" % (self.prems, self.schema, self.just))
else:
print ("\\ndl{%s}{%s}{}" % (self.prems, self.schema))
class Proof:
def __init__(self):
self.lines = []
self.outlines = set()
self.suppress = set()
self.note = ""
def addline(self, prems, schema, just):
self.lines.append(ProofLine(prems, schema, just))
def wholeproof(self,
note = "See the following pages for an explanation of the steps."):
self.outlines.clear()
self.suppress.clear()
self.note = note
for i in range(0, len(self.lines)):
self.outlines.add(i + 1)
self.plines()
def pproof(self, start, linelist):
self.outlines.clear()
self.suppress.clear()
for i in start:
self.outlines.add(i)
for l in linelist:
self.note = ""
if type(l) is list:
newlist = []
for num in l:
if type(num) is str:
self.note = num
continue
if type(num) is float:
# if we've already seen this, then the point is to print
# the citation this time.
if int(num) in self.outlines:
try:
self.suppress.remove(int(num))
except:
print("Failed sanity check!")
import sys
sys.exit(1)
else:
# we haven't seen it yet, so that means to suppress
# the citation until further notice
self.outlines.add(int(num))
self.suppress.add(int(num))
elif num < 0:
# don't suppress the citation
self.outlines.add(-num)
else:
self.outlines.add(num)
newlist.append(num)
self.plines(newlist)
continue
if type(l) is float:
# suppress the citation until further notice
self.outlines.add(int(l))
self.suppress.add(int(l))
self.plines()
continue
if l < 0:
# this means to go ahead and print the citation
# for that line.
self.suppress.discard(-l)
self.outlines.add(-l)
self.plines()
continue
# just a number
self.outlines.add(l)
self.plines([l])
def plines(self, thisone = []):
print("\\begin{ND}\n")
for i in range(0, len(self.lines)):
# so we don't have to mess with line 0.
lnum = i + 1
line = self.lines[i]
if lnum in self.outlines:
line.pout((not lnum in thisone) and (not lnum in self.suppress))
else:
line.dummy()
print("\\end{ND}\n")
if self.note:
print("\n\n%s\n\n" % (self.note))
print("\\clearpage\n\n")
#p = Proof()
#p.addline("1", "\\forall x(Fx \\to Gx)", "P")
#p.addline("2", "\\forall x(Gx \\to Hx)", "P")
#p.addline("3", "Fx", "P")
#p.addline("1", "Fx \\to Gx", "UI(1)")
#p.addline("1,3", "Gx", "TF(3,4)")
#p.addline("2", "Gx \\to Hx", "UI(2)")
#p.addline("1,2,3", "Hx", "TF(5,6)")
#p.addline("1,2", "Gx \\wedge Hx", "TF(5,7)")
#p.addline("1,2", "Fx \\to Gx \\wedge Hx", "D(8)[3]")
#p.addline("1,2", "\\forall x(Fx \\to Gx \\wedge Hx)", "UG(9)")
#p.pproof([1,2], [10, 9, [3,8], [5,7], -7, 4, 6, -7])
--
lyx-users mailing list
[email protected]
https://lists.lyx.org/mailman/listinfo/lyx-users
