論理学FAQのブログ

授業でもらったコメントに対して書いたリプライを、ブログ形式に編集しました。

授業動画公開:直観主義論理(3)(4)

直観主義論理シリーズ第3,4回です。予想通り、6本で終わりそうです。今回の2本はテクニカルな説明がメインでわりと無味乾燥でしょうか。

前期からやってきて、帰納法による証明をようやく導入しましたが、ちょっと遅い気もしますね。でも、前期の内容(古典論理・様相論理)だと、ありがたみのわかる場面があんまりないんですよね。

わたし自身は帰納法を使えるようになったときに初めて論理学がおもしろいと感じるようになったので、学生さんもそうだとうれしいんですが、どうでしょうね。

youtu.be

youtu.be

授業動画公開:厳密含意の論理

2020年度の後期授業が始まりました。コロナをめぐる状況も徐々に変わっていますが、前期と同じように授業動画を作って、共有させてもらおうと思います。

後期は厳密含意から始まります。

レジュメ

「正しい論理」を求めて:厳密含意の論理

動画

youtu.be

youtu.be

次回は直観主義論理、その後は多値論理、関連性論理、様相演算子としての否定(否定様相の論理)と続きます。

オンライン講義YouTube配信実録(11)―おまけ:機材・設定編

ありがたいことに、オンライン講義配信の技術的なことについて、学内で問い合わせをいただく機会が多くなってきました。そこで、機材や設定について少し細かくまとめておくことにします。すでに

takuro-logic.hatenablog.com

takuro-logic.hatenablog.com

takuro-logic.hatenablog.com

あたりにまとめてはいますが、改めてということで。いろいろ問題解決、改善など経た上での最終版です。まだベストとは言えませんが。

どういうタイプの講義を配信しているのかについてはこちらから見てください。シンポジウムとか違うタイプのイベントの配信はここからカスタマイズが必要になります (これから2つほどそういうイベントが控えています…)。

ハードウェア

画像のように配線します。講師の先生は自分でスライドを操作します。スライドの映像とカメラ(マイク音声含む)映像の2回線をAtem Mini Proに入力し、そこからMBPに入力します。Atem Mini Proは回線やPicture in Pictureの切り替えに使用します。

カメラは最初Lumix G8を使っていましたが、どうもきれいな映像にできなかったので、私物のA6400に変えました。気づいた人いるでしょうか。Atem Mini Proは4K入力は受け付けますが、出力は1080pなので基本的にすべて1080で動かしました。4K配信やってみたい!

ですが、じっさい多くのYouTuberが強調するように、だいじなのは映像より音声です。講義やセミナーであれば絶対にピンマイクをおすすめします。Wireless Go+AT9904は安心の組み合わせでした。

PCについては、配信ならほんとうはMacよりもWindows機のほうがやりやすく、しかもコスパがいいはずです。ただし絶対的な性能は必要なので、ゲーミングPCなど「やりすぎ」くらいのスペックのPCを用意するのをおすすめします。

それでもぜんぶで50万ほどあれば必要な機材は揃います。大学などある程度大きな組織であればどーんと揃えちゃえばいいんじゃないでしょうか。

オペ

講師の先生の研究室にお邪魔して設営して配信します。前もって下見に行って電源やLANの接続、明るさなどを確認しておきました。

毎回だいたい45分前から準備開始です。何もなければ時間的には余裕、何かトラブルがあってもリカバリー可能な時間です。

開始前
  • 機材設営(20分程度)後、ライブ配信テスト
  • 30分前:ツイッターで「このあとすぐ!」的ツイート
  • 5分前:カメラ録画開始 (念のため録画もしていました)
  • 3分前:Zoomミーティング開始 (YouTubeでの配信と同時に、少人数の学生さん相手にZoomも開いていました)
  • 2分前:YouTubeライブ配信開始 (流すのは画像スライドショー)
  • 1分前:iPhoneからTwitterライブ開始 (YouTubeへの誘導の役割)
  • 定刻:YouTubeをカメラ映像に切り替え、講義開始
講義中

じっさいに配信された動画はこちらからご覧ください。

  • 先生はスライドを操作しながら講義に集中
  • スイッチャーでカメラ画像・スライド・Picture in Pictureを切り替える
  • YouTubeチャット欄を中心に、ツイッター、Zoom、メールをチェック (家で見てるスタッフからメールでトラブル報告が来たりする)
  • チャット欄から質問を抜き出し、メモアプリにコピペする
  • 参考リンクをはったり、適当なコメントをしたり、チャット欄でちょっと遊ぶ
  • 質疑応答の時間になったらiPadを先生に渡し、メモアプリで質問を見て答えてもらう

けっこう忙しいです。ですが、これくらいなら分業するほどのものでもないかなと思います。分業したほうが意思疎通がめんどくさそうです。

終了後
  • 講義が終了したら、画像スライドショーに切り替えて配信は継続
  • Twitterライブ、カメラ録画は終了
  • YouTubeチャット欄に「ありがとうございました、次回もよろしく」コメントをして、YouTube配信終了
  • Zoomの学生さんたちと先生の質疑応答→Zoomも終了
  • 撤収

機材運搬・設営・撤収は多くの回で学生さんアルバイト1人に手伝ってもらいました。配信中の作業はワンオペです。アルバイト無しで1人で1日2回設営・配信・撤収をやると心身にかなりのダメージがあります笑

ソフトウェア:OBS

基本は、Atem Mini Proからの映像音声を受け取って、OBSYouTubeに配信します。配信用の主なパラメータ設定は以下のとおりです。

  • 映像ビットレート:6000kbps
  • エンコーダ:ソフトウェアエンコーダ (x264)
  • 音声ビットレート:160
  • エンコーダプリセット:medium
  • 音声サンプリングレート:48kHz
  • 基本(キャンバス)解像度:1920x1080
  • 出力(スケーリング)解像度:1920x1080

最初はもっと低いビットレート(たしか2000)でやっていたのですが、ネットやCPUの速度の様子を見ていると大丈夫そうだったので6000に上げました。少し映像はよくなった気がします。ネットは基本的に有線で約1Gbps出てたので余裕でしたし、CPU使用率は10%程度くらいに収まってました。もうちょっと攻められたかも。

OBSではその他に次のような機能を使いました。

  • 授業開始前と開始後に流すスライドショー (ソース→画像スライドショー)
  • PC内に保存している動画の再生 (ソース→メディアソース)
  • Slido (後述)のウィンドウキャプチャ (ソース→ウィンドウキャプチャ)

その他のソフトウェア

Zoom

Zoomに流す映像音声はNDI Virtual Input というプラグインを使って、OBSからのアウトプット(YouTubeへ配信するものと同じもの)を流していました。Zoomは電力を食うし、映像音声もあまりきれいでないので好きではありません。ただものすごいスピードで進化しているので目が離せません。

Slido

アンケート投票ウェブアプリです。リアルタイムで投票結果が表示されるので、参加体験マシマシです。カメラ・スライド映像との切り替えに気を遣いますが、それに見合うリターンはあります。詳しくは以下のエントリをどうぞ。

takuro-logic.hatenablog.com

メモ

macOS標準のメモアプリです。YouTubeライブのチャット欄から質問をコピペします(MBP上)。すると、iCloudを通じてiPadのメモアプリにそれが反映されます。質疑応答の時間中にどんどん来る質問もこれでリアルタイムに先生に伝達できました。便利。

 

前エントリ

takuro-logic.hatenablog.com

で述べたように、今回ここまでできたのは、私がかなり都合のよいポジションにいたからだと思うので、これからの課題はどうやって制度化するかですね。講義中の配信操作をする人間が純粋な技術スタッフでもなく純粋に内容のみにかかわるわけでもないので、誰がそこをやるのか難しいところかなと思います。

オンライン講義YouTube配信実録(10)―完結編

とくに新しい情報もないですが、シリーズ完結編です。合計26回のライブ配信、主に音ズレなど細かいことはあったものの、致命的なトラブルはなく終えることができました。開始3分前までネットが繋がらないとかいうヒヤリハット事案もあったんですが(わはは)、表面化しなくてよかったです。

とくに気をつけていたわけでもないですが、体調を崩すことなく完走できたのもホッとしました。時節柄、熱なんか出すとすべてストップしてしまいますからね。機材運びでギックリ腰やらずに済んだのも助かりました。

今回のシリーズでは、配信の技術的な事柄はほぼぜんぶ自分でやったんですが、やはりなかなかたいへんでした。それでも何とかなったのは:

  • ふだんからYouTubeを見まくっているせいで、カメラ、ガジェットや配信方法についてそれなりに知識があった
  • もともと遊軍的なポジションで比較的自由にできる時間があるのでそれを注ぎ込めた (自分の研究はできないし授業動画制作と重なって死、でしたが)
  • 裁量労働制()

などの要因があったからだと思います。レギュラーな仕事や会議の詰まっている教員や事務の方では難しいかなあという印象です。もちろん大学にはスーパーな方々が多数おられるのでやれてしまうんでしょうが、スーパーな方々のがんばりに期待するのはよくないです。

(で、これだけ時間注ぎ込んでも、ツイキャスとかインスタライブとかどうなのとか、調べられなかったことたくさんだし、ほんと時間が足りないですね。)

とはいえ、何と言ってもふだんとは桁違いの方々、そしてふだんとはちがう層の方々に見ていただけるので、ものすごくやりがいのある仕事ではありました。先生方の講義の素晴らしさありきの話ですが、やはりインターネットというのはすごいですね。ハード・ソフトの進歩もすごい。いったんこれを知ってしまったら元には戻れない感じです。ニューノーマル

これからどうなるんでしょうね。ノウハウ共有して戦力を増強したいところですが、さて。

f:id:takuro_logic:20200830223540j:plain

 

オンライン講義YouTube配信実録(9)― Atem miniとV-02HD

ひさしぶりの更新です。音ズレについては、前回書いた

takuro-logic.hatenablog.com

教えてもらった方法でやっています。それでも起こるときは起こりますね。起こったのは、「スライド+PinPでカメラ」からカメラ映像のみに切り替えたときです。しばらくすると、映像が早回しになる感じで動いて音声に追いつきます。このまま解決しないままシリーズは終わってしまいそうです。。。

 

これまたすごく細かい話ですが、以前

takuro-logic.hatenablog.com

takuro-logic.hatenablog.com

で書いた、スイッチャーにかんする、Atem mini (Pro)とV-02HDでは帯に短し襷に長しですね、という話。

どちらも解決方法はあるようで、Atem mini (Pro)の方は「マクロ」を使うということですね。いや、わかってはいたんですが、解説してくれてる動画があったので紹介します。

youtu.be

これで、

  • 設定したPinPのウィンドウの大きさや場所が保存されない
  • PinPの「主」と「従」が切り替えられない

という問題は解決できます。ただ、これは結局はソフトウェア上で切り替え操作をやることになるので、うーん。ハードウェアのボタンでポチッとやりたいですよねー。

V-02HDの方の弱点は、PinPのウィンドウの場所をワンボタンで変えられないということでしたが、こちらは、V-02HDをiPadとUSBでつないで、アプリで操作するという方法があるようです。

f:id:takuro_logic:20200824195536p:plain

f:id:takuro_logic:20200824195702p:plain

ウィンドウの大きさや位置の設定をpreset memoryとして複数記憶させておいて(上図)、それをiPad上でタップして切り替える(下図)ということのようです。音声に対するエフェクトも、というか基本全部これで操作できるスグレモノなんですが、まあ、iPadもう1枚持っていかないといけないのはちょっとキツい。でも、ガチの配信するならこれもありでしょうか。

Atem mini Pro ISOというのも出ましたがこれまた機能的に歯がゆいところで、お値段もそこそこ高くなってきました。決定版というものが出るのはもう少し先でしょうか。(ISOは、USB出力が2つあったら100%買いましたね。)

 

ともあれ、講義配信はあと1回です。いまのところ大きなトラブルなくこれているので、気を引き締めて参ります。

0項述語

とつぜん論理学ネタに復帰しますが。動画で言えばこのあたりです。

youtu.be

述語の項数

述語論理の原子式は項と述語からなるわけですが、述語には1項述語、2項述語、3項述語…と項数 (arity) が決められています。

日本語と対応させるなら「…は人間である」なんかが1項、「…は…を尊敬している」なんかが2項、「…は…と…の間にある」なんかが3項述語でしょうか。4項以上になると、さすがに自然言語には自然な対応物がなさそうですが、数学的にはいくらでも増やすことができます。

で、学生さんから、

では0項述語ってあるんでしょうか、あるとすればどういうものでしょう

という質問が来ました(意訳)。

答え:0項述語は、古典命題論理で出てきた命題変項のことです。日本語で言えば、文ですね。今回はこれを、モデルにおける付値の観点から説明します。

1項述語に対する付値

述語論理のモデルは、個体領域  D (空でない集合)とその上の付値 v からなります*1。付値は、述語論理の言語中の各語彙に、モデル中の何らかの数学的対象を割り当てます。

例えば1項述語 ( P とします) には、 Dの部分集合を割り当てます。要するに  D 中の個体のうち P を満たすものの集合ですね。つまり、

(*)  v(P) \subseteq D (1項述語の付値は D の部分集合)

です。ここではこれからの議論のために、これに対して別の見方をします。D の部分集合を1つ決めることは、 D から真理値  \{1,0\} への写像を1つ決めることにほかなりません (こういうのに慣れている人はしばらくスキップしてください)。

例えば、 D=\{a,b,c\}として、その部分集合を1つ、これも例えば

 X=\{a,b\} \subseteq D

と決めることは、D の要素のうち a b には「Yes (入っていいよ)」、 c には「No (入ってはいけないよ)」と決めることにほかなりません。そして、Yesを1、Noを0とするなら、これは

  •  a\mapsto 1
  •  b\mapsto 1
  •  c \mapsto 0

という写像を定めることにほかなりません。もちろん、反対に  D から  \{1,0\} への写像が1つ与えられたら、そこから  D の部分集合(yesと言われているやつら)を1つ決めることができます。

とすると、上の(*)は次のように書き換えることができます。

(**)  v(P)\in D\to \{1,0\} (1項述語の付値は D から \{1,0\}への写像)

ただし、 X\to YX から Y への写像全体の集合を表すものとします。すでに確認したように、(*)と(**)は同じことをちがう仕方で言っているだけです。

まあ、「…は人間である」という述語は「…」に入るモノに対して、「Yes」と「No」を返す関数ですよね (オオニシに対しては「Yes」、MacBookに対しては「No」等々)。だから、(**)の見方はごく自然なもののはずです。

n項述語に対する付値

2項述語の付値は  D^2=D\times D の部分集合、つまり、 D の要素のペアの集合でした。つまり、2項述語 P に対しては、

(*2)  v(P) \subseteq D^2

でした。先ほどと同じ見方の転換をすれば、これは

(**2)  v(P)\in D^2\to \{1,0\}

と言い換えることができます。つまり、各ペアに対して「Yes」と「No」を返す関数です。

もうおわかりかと思いますが、一般に  n 項述語 P に対しては、

(*n)  v(P) \subseteq D^n

であり、

(**n)  v(P)\in D^n\to \{1,0\}

です。先ほどの1項述語のときの (**) はこれの  n=1 の場合、すなわち、

(**1)  v(P)\in D^1\to \{1,0\}

に当たります。

0項述語に対する付値

さて、よくわからないながらも記号的に進めていけるのが数学のいいところです。以上を踏まえると、0項述語 (というものがあるとして) に対する付値は、

(**0)  v(P)\in D^0\to \{1,0\}

となるはずです。

集合の0乗

この  D^0 とは数の0乗 ( =1) と同じようなもので、あるいみ特別な集合です。すなわち、

 D^0=\{*\}

です。 * は何でもいいんだけど何らかの要素 ( D の要素とは関係ない) で、 \{ *\} とはその  * からなるシングルトン (単元集合) です。これは、この D に限った話ではなく、任意の集合  X に対して、

 X^0=\{ *\}

とすることができます *2

 \{*\} からの写像

さてでは次は、 D^0=\{*\} から \{1,0\} への写像とはどのようなものか考えてみましょう。2つしかないはずです。すなわち、

  •  f_1: *\mapsto 1 と割り当てる写像  f_1 か、
  •  f_0: *\mapsto 0 と割り当てる写像  f_0

しかありません。つまり、

 D^0\to \{1,0\} = \{ f_1, f_0\}

ですね。で、これって、

 D^0\to \{1,0\} = \{ f_1, f_0\}\cong \{1,0\}

ですね ( \cong は集合の同型)。

一般に、 \{*\} から集合  X への写像を1つ決めることは、(\{*\} に割り当てられる値として) 値域集合  X の要素を1つ決めることにほかならず、その逆も同様です。つまり、

 \{*\}\to X \cong X

です。 \{*\} から集合  X への写像の集合は、 X そのものと同一視できます。

0項述語=命題変項

これを踏まえると、(**0)は次のように書き換えられます。

(***0)  v(P)\in \{1,0\}

つまり、あるモデルにおける付値  vは、0項述語  P に対して1か0を割り当てる、ということです。付値によって1か0を割り当てられるものって何だったかと言うと、命題変項にほかなりません。ということで、0項述語とは命題変項のことやんかということになります。

 

以上は、0項述語というものがあるとすればそれは何かということを、述語論理のモデルの枠組みの中で数学的に整理しただけです。命題変項に対応する日本語の文というカテゴリーを「0項述語」と呼ぶことで何かおもしろいことがあるかというと、どうでしょう。無いんじゃないかなあ。

*1:このあたりはだいたい標準的な定義ですが、正確な定義はレジュメを見てください。

*2:この  \{ *\} は何かと言うと「掛け算の単位元」です。上で述べたとおり  1 です。というのは、任意の集合  X について、  \{*\} \times X\cong X\cong X\times \{*\} が成り立つからです ( \cong は集合としての同型関係、すなわち、全単射が存在するということを表します)。数の掛け算について  1\times x=x=x\times 1 が成り立つのと同じです。